Refactor reporters, allow positions which will get printed with lines

src/main/scala/leon/Reporter.scala

@@ -10,83 +10,157 @@ import purescala.PrettyPrinter
 import scala.annotation.implicitNotFound
 
 abstract class Reporter(settings: Settings) {
-  def infoFunction(msg: Any) : Unit
-  def warningFunction(msg: Any) : Unit
-  def errorFunction(msg: Any) : Unit
-  def debugFunction(msg: Any) : Unit
-  def fatalErrorFunction(msg: Any) : Nothing
 
-  // This part of the implementation is non-negociable.
+  abstract class Severity
+  case object INFO    extends Severity
+  case object WARNING extends Severity
+  case object ERROR   extends Severity
+  case object FATAL   extends Severity
+  case class  DEBUG(section: DebugSection) extends Severity
+
+  case class Message(severity: Severity, position: Position, msg: Any);
+
   private var _errorCount : Int = 0
   private var _warningCount : Int = 0
 
   final def errorCount : Int = _errorCount
   final def warningCount : Int = _warningCount
 
-  final def info(msg: Any) = infoFunction(msg)
-  final def warning(msg: Any) = {
-    _warningCount += 1
-    warningFunction(msg)
+  def account(msg: Message): Message = {
+    msg.severity match {
+      case WARNING       => _warningCount += 1
+      case ERROR | FATAL => _errorCount += 1
+      case _             =>
+    }
+
+    msg
   }
-  final def error(msg: Any) = {
-    _errorCount += 1
-    errorFunction(msg)
+
+  def emit(msg: Message): Unit
+
+  def onFatal(): Nothing = {
+    throw LeonFatalError(None)
   }
-  final def fatalError(msg: Any) = {
-    _errorCount += 1
-    fatalErrorFunction(msg)
+
+  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 fatalError(pos: Position, msg: Any): Nothing = {
+    emit(account(Message(FATAL, pos, msg)))
+    onFatal()
   }
 
+  def terminateIfError() = {
+    if (errorCount > 0) {
+      _errorCount = 0
+      _warningCount = 0
+      fatalError("There were errors.")
+    }
+  }
+
+  // Debugging
   private val debugMask = settings.debugSections.foldLeft(0){ _ | _.mask }
 
   def ifDebug(body: (Any => Unit) => Any)(implicit section: DebugSection) = {
     if ((debugMask & section.mask) == section.mask) {
-      body(debugFunction)
+      body( { (msg: Any) => emit(account(Message(DEBUG(section), NoPosition, msg))) } )
     }
   }
 
   def whenDebug(section: DebugSection)(body: (Any => Unit) => Any) {
     if ((debugMask & section.mask) == section.mask) {
-      body(debugFunction)
+      body( { (msg: Any) => emit(account(Message(DEBUG(section), NoPosition, msg))) } )
     }
   }
 
-  def debug(msg: => Any)(implicit section: DebugSection) = {
+
+  def debug(pos: Position, msg: => Any)(implicit section: DebugSection): Unit = {
     ifDebug{ debug =>
       debug(msg)
     }(section)
   }
+
+
+  // No-position alternatives
+  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 fatalError(msg: Any): Nothing = fatalError(NoPosition, msg)
+  final def debug(msg: => Any)(implicit section: DebugSection): Unit = debug(NoPosition, msg)
 }
 
 class DefaultReporter(settings: Settings) extends Reporter(settings) {
-  protected val errorPfx   = "[ Error ] "
-  protected val warningPfx = "[Warning] "
-  protected val infoPfx    = "[ Info  ] "
-  protected val fatalPfx   = "[ Fatal ] "
-  protected val debugPfx   = "[ Debug ] "
+  protected def severityToPrefix(sev: Severity): String = sev match {
+    case ERROR    => "["+Console.RED              +" Error "+Console.RESET+"]"
+    case WARNING  => "["+Console.YELLOW           +"Warning"+Console.RESET+"]"
+    case INFO     => "["+Console.BLUE             +" Info  "+Console.RESET+"]"
+    case FATAL    => "["+Console.RED+Console.BOLD +" Fatal "+Console.RESET+"]"
+    case DEBUG(_) => "["+Console.MAGENTA          +" Debug "+Console.RESET+"]"
+  }
 
-  def output(msg: String) : Unit = println(msg)
+  def emit(msg: Message) = {
+    val posString = if (msg.position != NoPosition) { msg.position+": " } else { "" }
 
-  protected def reline(pfx: String, msg: String) : String = {
-    val color = if(pfx == errorPfx || pfx == fatalPfx) {
-      Console.RED
-    } else if(pfx == warningPfx) {
-      Console.YELLOW
-    } else if(pfx == debugPfx) {
-      Console.MAGENTA
+    println(reline(severityToPrefix(msg.severity), posString + msg.msg.toString))
+    printLineContent(msg.position)
+  }
+
+  protected var linesOf = Map[java.io.File, List[String]]()
+
+  def getLine(pos: Position): Option[String] = {
+    val lines = linesOf.get(pos.file) match {
+      case Some(lines) =>
+        lines
+      case None =>
+        val lines = if (pos == NoPosition) {
+          Nil
+        } else {
+          scala.io.Source.fromFile(pos.file).getLines.toList
+        }
+
+        linesOf += pos.file -> lines
+        lines
+    }
+
+    if (lines.size > pos.line-1 && pos.line >= 0) {
+      Some(lines(pos.line-1))
     } else {
-      Console.BLUE
+      None
     }
-    "[" + color + pfx.substring(1, pfx.length-2) + Console.RESET + "] " +
-    msg.replaceAll("\n", "\n" + (" " * (pfx.size)))
   }
 
-  def errorFunction(msg: Any)   = output(reline(errorPfx, msg.toString))
-  def warningFunction(msg: Any) = output(reline(warningPfx, msg.toString))
-  def infoFunction(msg: Any)    = output(reline(infoPfx, msg.toString))
-  def debugFunction(msg: Any)   = output(reline(debugPfx, msg.toString))
-  def fatalErrorFunction(msg: Any) = {
-    output(reline(fatalPfx, msg.toString));
-    throw LeonFatalError(None)
+  val prefixSize = 10
+
+  val blankPrefix = " " * prefixSize
+
+  def printLineContent(pos: Position): Unit = {
+    getLine(pos) match {
+      case Some(line) =>
+        println(blankPrefix+line)
+        pos match {
+          case rp: RangePosition =>
+            val bp = rp.focusBegin
+            val ep = rp.focusEnd
+
+            val carret = if (bp.line == ep.line) {
+              val width = Math.max(ep.col - bp.col, 1)
+              ("^" * width)
+            } else {
+              val width = Math.max(line.length-bp.col, 1)
+              ("^" * width)+"..."
+            }
+
+            println(blankPrefix+(" " * (bp.col - 1) + Console.RED+carret+Console.RESET))
+
+          case op: OffsetPosition =>
+            println(blankPrefix+(" " * (op.col - 1) + Console.RED+"^"+Console.RESET))
+        }
+      case None =>
+    }
+  }
+
+  protected def reline(pfx: String, msg: String) : String = {
+    pfx+" "+msg.replaceAll("\n", "\n" + (" " * prefixSize))
   }
 }

src/test/scala/leon/test/TestSilentReporter.scala

@@ -4,5 +4,5 @@ package leon
 package test
 
 class TestSilentReporter extends DefaultReporter(Settings()) {
-  override def output(msg: String) : Unit = { }
+  override def emit(msg: Message): Unit = { }
 }