Refactor the error reporting code

The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.

1 files changed, 6 insertions, 6 deletions

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index 012ca4df..251d8656 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -29,7 +29,7 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Returns null on success, or an error string otherwise.

     /// </summary>

-    public static string ParseCheck(IList<string/*!*/>/*!*/ fileNames, string/*!*/ programName, out Program program)

+    public static string ParseCheck(IList<string/*!*/>/*!*/ fileNames, string/*!*/ programName, ErrorReporter reporter, out Program program)

       //modifies Bpl.CommandLineOptions.Clo.XmlSink.*;

     {

       Contract.Requires(programName != null);

@@ -47,20 +47,20 @@ namespace Microsoft.Dafny {
           Console.WriteLine("Parsing " + dafnyFileName);

         }

 

-        string err = ParseFile(dafnyFileName, Bpl.Token.NoToken, module, builtIns, new Errors());

+        string err = ParseFile(dafnyFileName, Bpl.Token.NoToken, module, builtIns, new Errors(reporter));

         if (err != null) {

           return err;

         }        

       }

 

       if (!DafnyOptions.O.DisallowIncludes) {

-        string errString = ParseIncludes(module, builtIns, fileNames, new Errors());

+        string errString = ParseIncludes(module, builtIns, fileNames, new Errors(reporter));

         if (errString != null) {

           return errString;

         }

       }

 

-      program = new Program(programName, module, builtIns);

+      program = new Program(programName, module, builtIns, reporter);

 

       MaybePrintProgram(program, DafnyOptions.O.DafnyPrintFile);

 

@@ -70,8 +70,8 @@ namespace Microsoft.Dafny {
       r.ResolveProgram(program);

       MaybePrintProgram(program, DafnyOptions.O.DafnyPrintResolvedFile);

 

-      if (r.ErrorCount != 0) {

-        return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, program.Name);

+      if (reporter.Count(ErrorLevel.Error) != 0) {

+        return string.Format("{0} resolution/type errors detected in {1}", reporter.Count(ErrorLevel.Error), program.Name);

       }

 

       return null;  // success