Clean up error reporting.

There now is one main entry point for reporting errors, warnings, or
information. Next step is to make the VS extension use that.

4 files changed, 34 insertions, 24 deletions

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index dae1b95e..53921bb1 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -4428,9 +4428,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 public class Errors {

 	public int count = 0;                                    // number of errors detected

-	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

-	public string errMsgFormat = "{0}({1},{2}): Error: {3}"; // 0=filename, 1=line, 2=column, 3=text

-	public string warningMsgFormat = "{0}({1},{2}): Warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

 

 	public void SynErr(string filename, int line, int col, int n) {

 		SynErr(filename, line, col, GetSyntaxErrorString(n));

@@ -4438,7 +4435,7 @@ public class Errors {
 

 	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

 		Contract.Requires(msg != null);

-		errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);

+		Dafny.Util.ReportIssue("Error", filename, line, col, msg);

 		count++;

 	}

 

@@ -4693,27 +4690,23 @@ public class Errors {
 		return s;

 	}

 

-	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {	// semantic errors

 		Contract.Requires(tok != null);

 		Contract.Requires(msg != null);

-		SemErr(tok.filename, tok.line, tok.col, msg);

+		Dafny.Util.ReportIssue("Error", tok, msg);

+		count++;

 	}

 

 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

 		Contract.Requires(msg != null);

-		errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);

+		Dafny.Util.ReportIssue("Error", filename, line, col, msg);

 		count++;

 	}

 

-	public void Warning(IToken/*!*/ tok, string/*!*/ msg) {  // warnings

+	public void Warning(IToken/*!*/ tok, string/*!*/ msg) {	 // warnings

 		Contract.Requires(tok != null);

 		Contract.Requires(msg != null);

-		Warning(tok.filename, tok.line, tok.col, msg);

-	}

-

-	public virtual void Warning(string filename, int line, int col, string msg) {

-		Contract.Requires(msg != null);

-		errorStream.WriteLine(warningMsgFormat, filename, line, col - 1, msg);

+		Dafny.Util.ReportIssue("Warning", tok, msg);

 	}

 } // Errors

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 44990d7d..e3083133 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -24,9 +24,7 @@ namespace Microsoft.Dafny
       Contract.Requires(msg != null);

       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Red;

-      Console.WriteLine("{0}({1},{2}): Error: {3}",

-          DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1,

-          string.Format(msg, args));

+      Dafny.Util.ReportIssue("Error", tok, msg, args);

       Console.ForegroundColor = col;

       ErrorCount++;

     }

@@ -66,9 +64,7 @@ namespace Microsoft.Dafny
       if (reportWarnings) {

         ConsoleColor col = Console.ForegroundColor;

         Console.ForegroundColor = ConsoleColor.Yellow;

-        Console.WriteLine("{0}({1},{2}): Warning: {3}",

-            DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1,

-            string.Format(msg, args));

+        Dafny.Util.ReportIssue("Warning", tok, msg, args);

         Console.ForegroundColor = col;

       }

     }

@@ -281,9 +277,7 @@ namespace Microsoft.Dafny
     }

 

     public static void DefaultInformationReporter(AdditionalInformation info) {

-      Console.WriteLine("{0}({1},{2}): Info: {3}",

-                        DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(info.Token.filename) : info.Token.filename,

-                        info.Token.line, info.Token.col - 1, info.Text);

+      Dafny.Util.ReportIssue("Info", info.Token, info.Text);

     }

 

     public void ResolveProgram(Program prog) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 05633742..e2c45558 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3609,7 +3609,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);

       var col = tok.col + (isEndToken ? tok.val.Length : 0);

-      string description = string.Format("{0}({1},{2}){3}{4}", tok.filename, tok.line, col, additionalInfo == null ? "" : ": ", additionalInfo ?? "");

+      string description = Util.ReportIssueToString_Bare(additionalInfo == null ? "" : ": ", tok.filename, tok.line, tok.col, additionalInfo ?? "");

       QKeyValue kv = new QKeyValue(tok, "captureState", new List<object>() { description }, null);

       return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv);

     }

diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs
index 63659696..6162d32c 100644
--- a/Source/Dafny/Util.cs
+++ b/Source/Dafny/Util.cs
@@ -67,6 +67,29 @@ namespace Microsoft.Dafny {
       return res;

     }

 

+    internal static void ReportIssue(string header, IToken tok, string msg, params object[] args) {

+      ReportIssue(header, tok, String.Format(msg, args));

+    }

+

+    internal static void ReportIssue(string header, IToken tok, string msg) {

+      ReportIssue(header, tok.filename, tok.line, tok.col, msg);

+    }

+

+    internal static void ReportIssue(string header, string filename, int line, int column, string msg) {

+      Console.WriteLine(ReportIssueToString(header, filename, line, column, msg));

+    }

+

+    internal static string ReportIssueToString(string header, string filename, int line, int column, string msg) {

+      Contract.Requires(header != null);

+      Contract.Requires(filename != null);

+      Contract.Requires(msg != null);

+      return ReportIssueToString_Bare(": " + header, filename, line, column, ": " + msg);

+    }

+

+    internal static string ReportIssueToString_Bare(string header, string filename, int line, int column, string msg) {

+      return String.Format("{0}({1},{2}){3}{4}", filename, line, column - 1, header, msg ?? "");

+    }

+

     /// <summary>

     /// Returns s but with all occurrences of '_' removed.

     /// </summary>