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, 7 insertions, 14 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