DafnyExtension: Improved the way errors (incl. locations) are kept up-to-date.

1 files changed, 18 insertions, 31 deletions

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index c7eba4c0..07bf33bf 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -142,7 +142,7 @@ namespace DafnyLanguage
       var currentSnapshot = spans[0].Snapshot;

       foreach (var err in AllErrors()) {

         if (err.Category != ErrorCategory.ProcessError) {

-          var span = err.Span().TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive);

+          var span = err.Span.TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive);

           string ty;  // the COLORs below indicate what I see on my machine

           switch (err.Category) {

             default:  // unexpected category

@@ -185,15 +185,14 @@ namespace DafnyLanguage
         return;  // we've already done this snapshot

       NormalizedSnapshotSpanCollection spans = new NormalizedSnapshotSpanCollection(new SnapshotSpan(snapshot, 0, snapshot.Length));

 

-      var driver = new DafnyDriver(snapshot.GetText(), _document != null ? _document.FilePath : "<program>");

+      var driver = new DafnyDriver(snapshot, _document != null ? _document.FilePath : "<program>");

       List<DafnyError> newErrors;

       Dafny.Program program;

       try {

         program = driver.ProcessResolution();

         newErrors = driver.Errors;

       } catch (Exception e) {

-        newErrors = new List<DafnyError>();

-        newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message));

+        newErrors = new List<DafnyError> { new DafnyError(0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message, snapshot) };

         program = null;

       }

 

@@ -216,13 +215,8 @@ namespace DafnyLanguage
 

     public void PopulateErrorList(List<DafnyError> newErrors, bool verificationErrors, ITextSnapshot snapshot) {

       Contract.Requires(newErrors != null);

-      foreach (var err in newErrors) {

-        if (err.Snapshot == null)

-        {

-          err.FillInSnapshot(snapshot);

-        }

-      }

-      if (verificationErrors) {

+

+       if (verificationErrors) {

         _verificationErrors = newErrors;

       } else {

         _resolutionErrors = newErrors;

@@ -231,16 +225,16 @@ namespace DafnyLanguage
       _errorProvider.SuspendRefresh();  // reduce flickering

       _errorProvider.Tasks.Clear();

       foreach (var err in AllErrors()) {

-        var l = err.Snapshot.GetLineFromLineNumber(err.Line);

-        var c = l.Start.Add(err.Column);

-        c = c.TranslateTo(_buffer.CurrentSnapshot, PointTrackingMode.Negative);

-        l = c.GetContainingLine();

+        var span = err.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive);

+        var lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);

+        var line = snapshot.GetLineFromPosition(span.Start.Position);

+        var columnNum = span.Start - line.Start;

         ErrorTask task = new ErrorTask() {

           Category = TaskCategory.BuildCompile,

           ErrorCategory = CategoryConversion(err.Category),

           Text = err.Message,

-          Line = l.LineNumber,

-          Column = l.Start.Difference(c)

+          Line = lineNum,

+          Column = columnNum

         };

         if (_document != null) {

           task.Document = _document.FilePath;

@@ -331,13 +325,14 @@ namespace DafnyLanguage
   {

     public readonly int Line;  // 0 based

     public readonly int Column;  // 0 based

-    public ITextSnapshot Snapshot;  // filled in during the FillInSnapshot call

+    public readonly ITextSnapshot Snapshot;

     public readonly ErrorCategory Category;

     public readonly string Message;

+    public readonly SnapshotSpan Span;

     /// <summary>

     /// "line" and "col" are expected to be 0-based

     /// </summary>

-    public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot = null) {

+    public DafnyError(int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot) {

       Contract.Requires(0 <= line);

       Contract.Requires(0 <= col);

       Line = line;

@@ -345,18 +340,10 @@ namespace DafnyLanguage
       Category = cat;

       Message = msg;

       Snapshot = snapshot;

-    }

-

-    public void FillInSnapshot(ITextSnapshot snapshot) {

-      Contract.Requires(snapshot != null);

-      Snapshot = snapshot;

-    }

-    public SnapshotSpan Span() {

-      Contract.Assume(Snapshot != null);  // requires that Snapshot has been filled in

-      var line = Snapshot.GetLineFromLineNumber(Line);

-      Contract.Assume(Column <= line.Length);  // this is really a precondition of the constructor + FillInSnapshot

-      var length = Math.Min(line.Length - Column, 5);

-      return new SnapshotSpan(line.Start + Column, length);

+      var sLine = Snapshot.GetLineFromLineNumber(line);

+      Contract.Assert(Column <= sLine.Length);

+      var sLength = Math.Max(0, Math.Min(sLine.Length - Column, 5));

+      Span = new SnapshotSpan(sLine.Start + Column, sLength);

     }

   }

 }