Merge pull request #131 from jad-hamza/ascii

Add option to remove colors and non-ascii characters, and to format errors for IDEs

Author: vkuncak

src/main/scala/inox/Main.scala

@@ -44,6 +44,7 @@ trait MainHelpers {
 
   protected def getOptions: Map[OptionDef[_], Description] = Map(
     optHelp -> Description(General, "Show help message"),
+    optNoColors -> Description(General, "Disable colored output and non-ascii characters (enable this option for better support in IDEs)"),
     optTimeout -> Description(General, "Set a timeout for the solver (in sec.)"),
     optSelectedSolvers -> Description(General, {
       "Use solvers s1,s2,...\nAvailable: " +
@@ -244,8 +245,9 @@ object Main extends MainHelpers {
         }
       }
 
+      val asciiOnly = ctx.options.findOptionOrDefault(optNoColors)
       ctx.reporter.whenDebug(utils.DebugSectionTimers) { debug =>
-        ctx.timers.outputTable(debug)
+        ctx.timers.outputTable(debug, asciiOnly)
       }
 
       exit(error = error)

src/main/scala/inox/Options.scala

@@ -231,3 +231,4 @@ object optSelectedSolvers extends SetOptionDef[String] {
   override def formatDefault: String = default.mkString(",")
 }
 
+object optNoColors extends inox.FlagOptionDef("no-colors", false)

src/main/scala/inox/Reporter.scala

@@ -182,7 +182,7 @@ class DefaultReporter(debugSections: Set[DebugSection]) extends Reporter(debugSe
 
   def emit(msg: Message) = synchronized {
     println(reline(severityToPrefix(msg.severity), smartPos(msg.position) + msg.msg.toString))
-    printLineContent(msg.position)
+    printLineContent(msg.position, false)
   }
 
   def getLine(pos: Position): Option[String] = {
@@ -201,10 +201,12 @@ class DefaultReporter(debugSections: Set[DebugSection]) extends Reporter(debugSe
 
   val blankPrefix = " " * prefixSize
 
-  def printLineContent(pos: Position): Unit = {
+  def printLineContent(pos: Position, asciiOnly: Boolean): Unit = {
     getLine(pos) match {
       case Some(line) =>
-        println(blankPrefix+line)
+        // Scala positions probably assume 1 tab = 8 spaces, so we replaces tabs
+        // for the carret (^) computed below to be aligned
+        println(blankPrefix+line.replace("\t", " " * 8))
         pos match {
           case rp: RangePosition =>
             val bp = rp.focusBegin
@@ -218,10 +220,16 @@ class DefaultReporter(debugSections: Set[DebugSection]) extends Reporter(debugSe
               ("^" * width)+"..."
             }
 
-            println(blankPrefix+(" " * (bp.col - 1) + Console.RED+carret+Console.RESET))
+            if (asciiOnly)
+              println(blankPrefix+(" " * (bp.col - 1) + carret))
+            else
+              println(blankPrefix+(" " * (bp.col - 1) + Console.RED+carret+Console.RESET))
 
           case op: OffsetPosition =>
-            println(blankPrefix+(" " * (op.col - 1) + Console.RED+"^"+Console.RESET))
+            if (asciiOnly)
+              println(blankPrefix+(" " * (op.col - 1) + "^"))
+            else
+              println(blankPrefix+(" " * (op.col - 1) + Console.RED+"^"+Console.RESET))
         }
       case None =>
     }
@@ -234,12 +242,26 @@ class DefaultReporter(debugSections: Set[DebugSection]) extends Reporter(debugSe
 }
 
 class PlainTextReporter(debugSections: Set[DebugSection]) extends DefaultReporter(debugSections) {
-  override protected def severityToPrefix(sev: Severity): String = sev match {
-    case ERROR    => "[ Error  ]"
-    case WARNING  => "[Warning ]"
-    case INFO     => "[  Info  ]"
-    case FATAL    => "[ Fatal  ]"
-    case INTERNAL => "[Internal]"
-    case DEBUG(_) => "[ Debug  ]"
+  override protected def severityToPrefix(sev: Severity): String = ""
+
+  protected def severityToString(sev: Severity): String = sev match {
+    case ERROR    => "error"
+    case WARNING  => "warning"
+    case INFO     => "info"
+    case FATAL    => "fatal"
+    case INTERNAL => "internal"
+    case DEBUG(_) => "debug"
+  }
+
+  override def emit(msg: Message) = synchronized {
+    if (msg.severity == ERROR || msg.severity == FATAL || msg.severity == INTERNAL)
+      println(smartPos(msg.position) + "error: " + msg.msg.toString)
+    else if (msg.severity == WARNING)
+      println(smartPos(msg.position) + "warning: " + msg.msg.toString)
+    else if (msg.severity.isInstanceOf[DEBUG])
+      println(smartPos(msg.position) + "debug: " + msg.msg.toString)
+    else
+      println(smartPos(msg.position) + msg.msg.toString)
+    printLineContent(msg.position, true)
   }
 }

src/main/scala/inox/utils/ASCIIHelpers.scala

@@ -64,24 +64,42 @@ object ASCIIHelpers {
       (0 until cellsPerRow).map(i => constraints.getOrElse((i, i), 1))
     }
 
-    def render: String = {
+    def render(asciiOnly: Boolean): String = {
       val colSizes = computeColumnSizes
       val titleWidth = trimNonPrintable(title).length
       val fullWidth = Math.max(colSizes.sum + colSizes.size * 2, titleWidth + 7)
       val padWidth = fullWidth - titleWidth - 5
 
       val sb = new StringBuffer
 
-      sb append "  ┌─" + ("─" * titleWidth) + "─┐\n"
-      sb append "╔═╡ " +         title      + " ╞"  + ("═" * padWidth) + "╗\n"
-      sb append "║ └─" + ("─" * titleWidth) + "─┘"  + (" " * padWidth) + "║\n"
+      val barH = if (asciiOnly) "#" else "─"
+      val topLeft = if (asciiOnly) "#" else "┌"
+      val topRight = if (asciiOnly) "#" else "┐"
+      val bottomLeft = if (asciiOnly) "#" else "└"
+      val bottomRight = if (asciiOnly) "#" else "┘"
+      val dots = if (asciiOnly) "." else "┄"
+      val doubleBarH = if (asciiOnly) "#" else "═"
+      val doubleBarV = if (asciiOnly) "#" else "║"
+      val doubleTopLeft = if (asciiOnly) "#" else "╔"
+      val doubleTopRight = if (asciiOnly) "#" else "╗"
+      val doubleBottomLeft = if (asciiOnly) "#" else "╚"
+      val doubleBottomRight = if (asciiOnly) "#" else "╝"
+
+      val leftConnect = if (asciiOnly) "#" else "╡"
+      val rightConnect = if (asciiOnly) "#" else "╞"
+      val doubleRightConnect = if (asciiOnly) "#" else "╟"
+      val doubleLeftConnect = if (asciiOnly) "#" else "╢"
+
+      sb append s"  $topLeft$barH" + (barH * titleWidth) + s"$barH$topRight\n"
+      sb append s"$doubleTopLeft$doubleBarH$leftConnect " + title + s" $rightConnect" + (doubleBarH * padWidth) + s"$doubleTopRight\n"
+      sb append s"$doubleBarV $bottomLeft$barH" + (barH * titleWidth) + s"$barH$bottomRight"  + (" " * padWidth) + s"$doubleBarV\n"
 
       for (r <- rows) r match {
         case Separator =>
-          sb append "╟" + ("┄" * fullWidth) + "╢\n"
+          sb append doubleRightConnect + (dots * fullWidth) + s"$doubleLeftConnect\n"
 
         case Row(cells) =>
-          sb append "║ "
+          sb append s"$doubleBarV "
           var i = 0
           for (c <- cells) {
             if (i > 0) {
@@ -102,10 +120,10 @@ object ASCIIHelpers {
 
             i += c.spanning
           }
-          sb append " ║\n"
+          sb append s" $doubleBarV\n"
       }
 
-      sb append "╚" + ("═" * fullWidth) + "╝"
+      sb append doubleBottomLeft + (doubleBarH * fullWidth) + doubleBottomRight
 
       sb.toString
     }

src/main/scala/inox/utils/Timer.scala

@@ -100,7 +100,7 @@ final class TimerStorage private(val _name: Option[String])
    *
    * NOTE All timers must have been stopped before calling this method.
    */
-  def outputTable(printer: String => Unit): Unit = {
+  def outputTable(printer: String => Unit, asciiOnly: Boolean): Unit = {
     import utils.ASCIIHelpers.{ Cell, Right, Row, Separator, Table }
 
     var table = Table("Timers")
@@ -148,7 +148,7 @@ final class TimerStorage private(val _name: Option[String])
     }
 
     rec("", this)
-    printer(table.render)
+    printer(table.render(asciiOnly))
   }
 }