DafnyExtension: Fixed flickering of errors in the error list.

1 files changed, 27 insertions, 23 deletions

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index b5e347dc..33baf3b5 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -109,6 +109,7 @@ namespace DafnyLanguage
           }

         }

         entry.Errors.Push(error);

+        UpdateErrorList(Snapshot);

       }

     }

 

@@ -306,33 +307,36 @@ namespace DafnyLanguage
 

     public void UpdateErrorList(ITextSnapshot snapshot)

     {

-      _errorProvider.SuspendRefresh();  // reduce flickering

-      _errorProvider.Tasks.Clear();

-      foreach (var err in AllErrors)

+      lock (this)

       {

-        var span = err.Span.GetSpan(snapshot);

-        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 = lineNum,

-          Column = columnNum

-        };

-        if (_document != null)

-        {

-          task.Document = _document.FilePath;

-        }

-        if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)

+        _errorProvider.SuspendRefresh();  // reduce flickering

+        _errorProvider.Tasks.Clear();

+        foreach (var err in AllErrors)

         {

-          task.Navigate += new EventHandler(NavigateHandler);

+          var span = err.Span.GetSpan(snapshot);

+          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 = lineNum,

+            Column = columnNum

+          };

+          if (_document != null)

+          {

+            task.Document = _document.FilePath;

+          }

+          if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)

+          {

+            task.Navigate += new EventHandler(NavigateHandler);

+          }

+          _errorProvider.Tasks.Add(task);

         }

-        _errorProvider.Tasks.Add(task);

+        _errorProvider.ResumeRefresh();

       }

-      _errorProvider.ResumeRefresh();

       var chng = TagsChanged;

       if (chng != null)

         chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));