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.

1 files changed, 23 insertions, 0 deletions

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>