Improve help message

src/main/scala/leon/LeonOption.scala

@@ -15,7 +15,7 @@ abstract class LeonOptionDef[+A] {
     else s"--$name=$usageRhs"
   }
   def helpString = {
-    f"$usageDesc%-22s" + description.replaceAll("\n", "\n" + " " * 22)
+    f"$usageDesc%-26s" + description.replaceAll("\n", "\n" + " " * 26)
   }
 
   private def parseValue(s: String)(implicit reporter: Reporter): A = {

src/main/scala/leon/Main.scala

@@ -51,19 +51,20 @@ object Main {
   lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
 
   def displayHelp(reporter: Reporter, error: Boolean) = {
-    reporter.info(MainComponent.description)
+
+    reporter.title(MainComponent.description)
     for (opt <- MainComponent.definedOptions.toSeq.sortBy(_.name)) {
       reporter.info(opt.helpString)
     }
     reporter.info("")
 
-    reporter.info("Additional top-level options")
+    reporter.title("Additional top-level options")
     for (opt <- SharedOptions.definedOptions.toSeq.sortBy(_.name)) {
       reporter.info(opt.helpString)
     }
     reporter.info("")
       
-    reporter.info("Additional options, by component:")
+    reporter.title("Additional options, by component:")
 
     for (c <- (allComponents - MainComponent - SharedOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
       reporter.info("")
@@ -77,7 +78,7 @@ object Main {
   }
 
   def displayVersion(reporter: Reporter) = {
-    reporter.info("Leon verification and synthesis tool (http://leon.epfl.ch/)")
+    reporter.title("Leon verification and synthesis tool (http://leon.epfl.ch/)")
     reporter.info("")
   }
 

src/main/scala/leon/Reporter.scala

@@ -43,6 +43,7 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
   final def info(pos: Position, msg: Any): Unit    = emit(account(Message(INFO, pos, msg)))
   final def warning(pos: Position, msg: Any): Unit = emit(account(Message(WARNING, pos, msg)))
   final def error(pos: Position, msg: Any): Unit   = emit(account(Message(ERROR, pos, msg)))
+  final def title(pos: Position, msg: Any): Unit   = emit(account(Message(INFO, pos, Console.BOLD + msg + Console.RESET)))
 
   final def fatalError(pos: Position, msg: Any): Nothing = {
     emit(account(Message(FATAL, pos, msg)))
@@ -97,6 +98,7 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
   final def info(msg: Any): Unit          = info(NoPosition, msg)
   final def warning(msg: Any): Unit       = warning(NoPosition, msg)
   final def error(msg: Any): Unit         = error(NoPosition, msg)
+  final def title(msg: Any): Unit         = title(NoPosition, msg)
   final def fatalError(msg: Any): Nothing = fatalError(NoPosition, msg)
   final def internalError(msg: Any) : Nothing = internalError(NoPosition, msg)
   final def internalAssertion(cond : Boolean, msg: Any) : Unit = internalAssertion(cond,NoPosition, msg)

src/main/scala/leon/SharedOptions.scala

@@ -22,7 +22,7 @@ object SharedOptions extends LeonComponent {
     val usageRhs = "f1,f2,..."
   }
 
-  val optEval = LeonStringOptionDef("eval", "Evaluate ground functions", "default", "--eval[=code|default]")
+  val optEval = LeonStringOptionDef("eval", "Evaluate ground functions", "default", "[code|default]")
 
   val optSelectedSolvers = new LeonOptionDef[Set[String]] {
     val name = "solvers"