From d60c518a66207cf215eb21cab4dd300569244694 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 23 Apr 2015 17:53:53 +0200
Subject: [PATCH] Some pretty printing improvements for options
---
src/main/scala/leon/LeonOption.scala | 3 +--
src/main/scala/leon/Main.scala | 7 +++++++
2 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index d3d65b4f3..e8b653a5b 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -15,8 +15,7 @@ abstract class LeonOptionDef[+A] {
else s"--$name=$usageRhs"
}
def helpString = {
- val (hd :: tl) = description.split("\n").toList
- (f"$usageDesc%-21s $hd" :: ( tl map (" " * 22 + _))).mkString("\n")
+ f"$usageDesc%-22s" + description.replaceAll("\n", "\n" + " " * 22)
}
private def parseValue(s: String)(implicit reporter: Reporter): A = {
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 72e8c3fb9..e9eb7b6e5 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -51,6 +51,7 @@ object Main {
lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
def displayHelp(reporter: Reporter, error: Boolean) = {
+ reporter.info("Top-level options:")
reporter.info("")
for (opt <- (MainComponent.definedOptions ++ SharedOptions.definedOptions).toSeq.sortBy(_.name)) {
@@ -70,6 +71,11 @@ object Main {
exit(error)
}
+ def displayVersion(reporter: Reporter) = {
+ reporter.info("Leon verification and synthesis tool (http://leon.epfl.ch/)")
+ reporter.info("")
+ }
+
private def exit(error: Boolean) = sys.exit(if (error) 1 else 0)
def processOptions(args: Seq[String]): LeonContext = {
@@ -133,6 +139,7 @@ object Main {
val verifyF = ctx.findOptionOrDefault(optVerify)
if (helpF) {
+ displayVersion(ctx.reporter)
displayHelp(ctx.reporter, error = false)
} else {
val pipeBegin: Pipeline[List[String], Program] =
--
GitLab