From a04534f253aa31ed94614c236307764f08a38621 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 23 Apr 2015 16:21:07 +0200
Subject: [PATCH] Multiline help, improvements
---
src/main/scala/leon/LeonOption.scala | 10 ++++++----
src/main/scala/leon/Main.scala | 7 +------
src/main/scala/leon/SharedOptions.scala | 2 +-
src/main/scala/leon/solvers/SolverFactory.scala | 7 ++++++-
4 files changed, 14 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index a62abbfff..d3d65b4f3 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -14,8 +14,10 @@ abstract class LeonOptionDef[+A] {
if (usageRhs.isEmpty) s"--$name"
else s"--$name=$usageRhs"
}
- def usageDescs = usageDesc.split("\n").toList
- def helpString = f"${usageDesc}%-21s ${description}"
+ def helpString = {
+ val (hd :: tl) = description.split("\n").toList
+ (f"$usageDesc%-21s $hd" :: ( tl map (" " * 22 + _))).mkString("\n")
+ }
private def parseValue(s: String)(implicit reporter: Reporter): A = {
try { parser(s) }
@@ -83,10 +85,10 @@ object OptionParsers {
case _ => throw new IllegalArgumentException
}
def seqParser[A](base: OptionParser[A]): OptionParser[Seq[A]] = s => {
- s.split(",").map(base)
+ s.split(",").filter(_.nonEmpty).map(base)
}
def setParser[A](base: OptionParser[A]): OptionParser[Set[A]] = s => {
- s.split(",").map(base).toSet
+ s.split(",").filter(_.nonEmpty).map(base).toSet
}
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 153a28a76..17f431413 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -54,12 +54,7 @@ object Main {
reporter.info("")
for (opt <- (MainComponent.definedOptions ++ SharedOptions.definedOptions).toSeq.sortBy(_.name)) {
- val (uhead :: utail) = opt.usageDescs
- reporter.info(f"${opt.usageDesc}%-20s ${uhead}")
- for(u <- utail) {
- reporter.info(f"${""}%-20s ${u}")
- }
-
+ reporter.info(opt.helpString)
}
reporter.info("")
reporter.info("Additional options, by component:")
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index 41dfe68df..a5e7e6635 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -22,7 +22,7 @@ object SharedOptions extends LeonComponent {
case object SelectedSolvers extends LeonOptionDef[Set[String]] {
val name = "solvers"
- val description = "Use solvers s1, s2, ... in parallel (default: fairz3)"
+ val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
val default = Set("fairz3")
val parser = setParser(stringParser)
val usageRhs = "s1,s2,..."
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index c897fc259..21a56c5b4 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -29,6 +29,11 @@ object SolverFactory {
"unrollz3" -> "Native Z3 with leon-templates for unfolding",
"enum" -> "Enumeration-based counter-example-finder"
)
+
+ val availableSolversPretty = "Available: " +
+ solvers.SolverFactory.definedSolvers.toSeq.sortBy(_._1).map {
+ case (name, desc) => f"\n $name%-14s : $desc"
+ }.mkString("")
def getFromSettings(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
getFromName(ctx, program)(ctx.findOptionOrDefault(SharedOptions.SelectedSolvers).toSeq : _*)
@@ -71,7 +76,7 @@ object SolverFactory {
}
def showSolvers() = {
- ctx.reporter.error("Available:\n" + definedSolvers.map {" - " + _}.mkString("\n"))
+ ctx.reporter.error(availableSolversPretty)
ctx.reporter.fatalError("Aborting Leon...")
}
--
GitLab