diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index e5015a46dc12553db9f3f6c7086aa90943c76814..4e4963bdbc22c6a72bd6953c6761fa6af0ddcec3 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/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))
}
}
diff --git a/src/test/scala/leon/test/TestSilentReporter.scala b/src/test/scala/leon/test/TestSilentReporter.scala
index 295c04be176d695648ec9bc5aab93c86dbf96758..ab12c99509c116c57061f37df01d07286882b35a 100644
--- a/src/test/scala/leon/test/TestSilentReporter.scala
+++ b/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 = { }
}