Revert change 1997 (bfe7c149bef1). IDE performance. Don't delay the resolver

until the editor is idle for 5 second.

1 files changed, 5 insertions, 33 deletions

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index b711c276..4a50a4e8 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -15,7 +15,6 @@ using System.Linq;
 using System.Text.RegularExpressions;

 using System.Windows.Shapes;

 using Microsoft.VisualStudio;

-using System.Windows.Threading;

 using Microsoft.VisualStudio.Shell;

 using Microsoft.VisualStudio.Shell.Interop;

 using Microsoft.VisualStudio.Text;

@@ -130,8 +129,6 @@ namespace DafnyLanguage
     ErrorListProvider _errorProvider;

     private bool m_disposed;

 

-    readonly DispatcherTimer timer;

-

     // The 'Snapshot' and 'Program' fields should be updated and read together, so they are protected by "this"

     public ITextSnapshot Snapshot;  // may be null

     public Dafny.Program Program;  // non-null only if the snapshot contains a Dafny program that type checks

@@ -230,13 +227,7 @@ namespace DafnyLanguage
       Snapshot = null;  // this makes sure the next snapshot will look different

       _errorProvider = new ErrorListProvider(serviceProvider);

 

-      BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, UponIdle);

-

-      // keep track idle time after BufferIdleEvent has been handled.

-      timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle);

-      timer.Interval = TimeSpan.FromMilliseconds(5000);

-      timer.Tick += new EventHandler(ResolveBuffer);

-      buffer.Changed += BufferChanged;

+      BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer);

     }

 

     public void Dispose()

@@ -266,9 +257,7 @@ namespace DafnyLanguage
               _errorProvider.Dispose();

               _errorProvider = null;

             }

-            BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, UponIdle);

-            timer.Tick -= ResolveBuffer;

-            _buffer.Changed -= BufferChanged;

+            BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);

             if (_document != null && _document.TextBuffer != null)

             {

               ResolverTaggers.Remove(_document.TextBuffer);

@@ -328,21 +317,9 @@ namespace DafnyLanguage
     /// <summary>

     /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly.

     /// </summary>

-    void ResolveBuffer(object sender, EventArgs args)

-    {

-      timer.Stop();

-      ParseAndResolveBuffer(sender, args, true);

-    }

-

-    void UponIdle(object sender, EventArgs args) {

-      timer.Stop();

-      ParseAndResolveBuffer(sender, args, false);

-      timer.Start();

-    }

-

-    void ParseAndResolveBuffer(object sender, EventArgs args, bool runResolver) {

+    void ResolveBuffer(object sender, EventArgs args) {

       ITextSnapshot snapshot = _buffer.CurrentSnapshot;

-      if (snapshot == Snapshot && !runResolver)

+      if (snapshot == Snapshot)

         return;  // we've already done this snapshot

 

       string filename = _document != null ? _document.FilePath : "<program>";

@@ -351,7 +328,7 @@ namespace DafnyLanguage
       Dafny.Program program;

       try

       {

-        program = driver.ProcessResolution(runResolver);

+        program = driver.ProcessResolution(true);

         newErrors = driver.Errors;

       }

       catch (Exception e)

@@ -380,11 +357,6 @@ namespace DafnyLanguage
       UpdateErrorList(snapshot);

     }

 

-    void BufferChanged(object sender, TextContentChangedEventArgs e) {

-      timer.Stop();

-      timer.Start();

-    }

-

     public void UpdateErrorList(ITextSnapshot snapshot)

     {

       if (_errorProvider != null && !m_disposed)