From 753f812b083867675294ab569c431bcbfd8b738b Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 6 Jan 2015 16:56:26 +0100
Subject: [PATCH] Bring back reporter with colors, and some corrections
---
src/main/scala/leon/Main.scala | 2 +-
src/main/scala/leon/Reporter.scala | 23 ++++++++++++-----------
2 files changed, 13 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 30e4152c6..49ab85e95 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -179,7 +179,7 @@ object Main {
}
// Create a new reporter taking settings into account
- val reporter = new PlainTextReporter(settings)
+ val reporter = new DefaultReporter(settings)
reporter.whenDebug(DebugSectionOptions) { debug =>
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 113c9ab87..cc39c108e 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -106,12 +106,12 @@ abstract class Reporter(settings: Settings) {
class DefaultReporter(settings: Settings) extends Reporter(settings) {
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 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 INTERNAL => "["+ Console.BOLD +"Internal"+Console.RESET+"]"
- case DEBUG(_) => "["+Console.MAGENTA +" Debug "+Console.RESET+"]"
+ case DEBUG(_) => "["+Console.MAGENTA +" Debug "+Console.RESET+"]"
}
def emit(msg: Message) = {
@@ -145,7 +145,7 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
}
}
- val prefixSize = 10
+ val prefixSize = 11
val blankPrefix = " " * prefixSize
@@ -183,10 +183,11 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
class PlainTextReporter(settings: Settings) extends DefaultReporter(settings) {
override protected def severityToPrefix(sev: Severity): String = sev match {
- case ERROR => "[ Error ]"
- case WARNING => "[Warning]"
- case INFO => "[ Info ]"
- case FATAL => "[ Fatal ]"
- case DEBUG(_) => "[ Debug ]"
+ case ERROR => "[ Error ]"
+ case WARNING => "[Warning ]"
+ case INFO => "[ Info ]"
+ case FATAL => "[ Fatal ]"
+ case INTERNAL => "[Internal]"
+ case DEBUG(_) => "[ Debug ]"
}
}
--
GitLab