VS IDE performance - invoke dafny parser when the buffer hasn't changed for

half a second, but delay calling Dafny resolver until the text buffer hasn't
been changed for 5 seconds. Also save the parsing result from TokenTagger in
ITextBuffer's property instead of in a static field.

3 files changed, 82 insertions, 35 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 27471d56..037d0cd3 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -18,13 +18,16 @@ namespace DafnyLanguage
   {

     readonly string _filename;

     readonly ITextSnapshot _snapshot;

+    readonly ITextBuffer _buffer;

     Dafny.Program _program;

+    static object bufferDafnyKey = new object();

 

     List<DafnyError> _errors = new List<DafnyError>();

     public List<DafnyError> Errors { get { return _errors; } }

 

-    public DafnyDriver(ITextSnapshot snapshot, string filename) {

-      _snapshot = snapshot;

+    public DafnyDriver(ITextBuffer buffer, string filename) {

+      _buffer = buffer;

+      _snapshot = buffer.CurrentSnapshot;

       _filename = filename;

     }

 

@@ -107,25 +110,42 @@ namespace DafnyLanguage
 

     #region Parsing and type checking

 

-    internal Dafny.Program ProcessResolution() {

-      if (!ParseAndTypeCheck()) {

+    internal Dafny.Program ProcessResolution(bool runResolver) {

+      if (!ParseAndTypeCheck(runResolver)) {

         return null;

       }

       return _program;

     }

 

-    bool ParseAndTypeCheck() {

-      Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);

-      Dafny.BuiltIns builtIns = new Dafny.BuiltIns();

-

+    bool ParseAndTypeCheck(bool runResolver) {

+      Tuple<ITextSnapshot, Dafny.Program, List<DafnyError>> parseResult;

+      Dafny.Program program;

       var errorReporter = new VSErrorReporter(this);

-      var parseErrors = new Dafny.Errors(errorReporter);

-

-      int errorCount = Dafny.Parser.Parse(_snapshot.GetText(), _filename, _filename, module, builtIns, parseErrors);

-      string errString = Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), parseErrors);

-      if (errorCount != 0 || errString != null)

+      if (_buffer.Properties.TryGetProperty(bufferDafnyKey, out parseResult) &&

+         (parseResult.Item1 == _snapshot)) {

+        // already parsed;

+        program = parseResult.Item2;

+        _errors = parseResult.Item3;

+        if (program == null)

+          runResolver = false;

+      } else {

+        Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);

+        Dafny.BuiltIns builtIns = new Dafny.BuiltIns();

+        var parseErrors = new Dafny.Errors(errorReporter);

+        int errorCount = Dafny.Parser.Parse(_snapshot.GetText(), _filename, _filename, module, builtIns, parseErrors);

+        string errString = Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), parseErrors);

+

+        if (errorCount != 0 || errString != null) {

+          runResolver = false;

+          program = null;

+        } else {

+          program = new Dafny.Program(_filename, module, builtIns, errorReporter);

+        }

+        _buffer.Properties[bufferDafnyKey] = new Tuple<ITextSnapshot, Dafny.Program, List<DafnyError>>(_snapshot, program, _errors);

+      }

+      if (!runResolver) {

         return false;

-      Dafny.Program program = new Dafny.Program(_filename, module, builtIns, errorReporter);

+      }

 

       var r = new Resolver(program);

       r.ResolveProgram(program);

@@ -136,6 +156,7 @@ namespace DafnyLanguage
       return true;  // success

     }

 

+

     void RecordError(string filename, int line, int col, ErrorCategory cat, string msg, bool isRecycled = false)

     {

       _errors.Add(new DafnyError(filename, line - 1, col - 1, cat, msg, _snapshot, isRecycled, null, System.IO.Path.GetFullPath(this._filename) == filename));

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 58a46196..b711c276 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -15,6 +15,7 @@ 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;

@@ -129,6 +130,8 @@ 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

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

       _errorProvider = new ErrorListProvider(serviceProvider);

 

-      BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer);

+      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;

     }

 

     public void Dispose()

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

               _errorProvider = null;

             }

-            BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);

+            BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, UponIdle);

+            timer.Tick -= ResolveBuffer;

+            _buffer.Changed -= BufferChanged;

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

             {

               ResolverTaggers.Remove(_document.TextBuffer);

@@ -319,17 +330,28 @@ namespace DafnyLanguage
     /// </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) {

       ITextSnapshot snapshot = _buffer.CurrentSnapshot;

-      if (snapshot == Snapshot)

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

         return;  // we've already done this snapshot

 

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

-      var driver = new DafnyDriver(snapshot, filename);

+      var driver = new DafnyDriver(_buffer, filename);

       List<DafnyError> newErrors;

       Dafny.Program program;

       try

       {

-        program = driver.ProcessResolution();

+        program = driver.ProcessResolution(runResolver);

         newErrors = driver.Errors;

       }

       catch (Exception e)

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

     }

 

+    void BufferChanged(object sender, TextContentChangedEventArgs e) {

+      timer.Stop();

+      timer.Start();

+    }

+

     public void UpdateErrorList(ITextSnapshot snapshot)

     {

       if (_errorProvider != null && !m_disposed)

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index f1c4860c..7a5eb572 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -91,10 +91,7 @@ namespace DafnyLanguage
     ITextBuffer _buffer;

     ITextSnapshot _snapshot;

     List<TokenRegion> _regions;

-    // TODO: instead of storing the scan result in the static field and shared by the different

-    // instances of DafnyTokenTagger, could it be associated to the TextBuffer using 

-    // ITextBuffer.Properties.GetOrCreateSingletonProperty?

-    static ScanResult _scanResult = null;

+    static object bufferTokenTaggerKey = new object();

     bool _disposed;

 

     internal DafnyTokenTagger(ITextBuffer buffer) {

@@ -109,10 +106,10 @@ namespace DafnyLanguage
       lock (this) {

         if (!_disposed) {

           _buffer.Changed -= ReparseFile;

+          _buffer.Properties.RemoveProperty(bufferTokenTaggerKey);

           _buffer = null;

           _snapshot = null;

           _regions = null;

-          _scanResult = null;

           _disposed = true;

         }

       }

@@ -150,12 +147,13 @@ namespace DafnyLanguage
         return;  // we've already computed the regions for this snapshot

       

       NormalizedSnapshotSpanCollection difference = new NormalizedSnapshotSpanCollection();

-      if (DafnyTokenTagger._scanResult != null &&

-        DafnyTokenTagger._scanResult._oldSnapshot == _snapshot &&

-        DafnyTokenTagger._scanResult._newSnapshot == snapshot) {

-        difference = DafnyTokenTagger._scanResult._difference;

+      ScanResult result;

+      if (_buffer.Properties.TryGetProperty(bufferTokenTaggerKey, out result) &&

+          (result._oldSnapshot == _snapshot) &&

+          (result._newSnapshot == snapshot)) {

+        difference = result._difference;

         // save the new baseline

-        _regions = DafnyTokenTagger._scanResult._regions;

+        _regions = result._regions;

         _snapshot = snapshot;

       } else {

         List<TokenRegion>  regions = new List<TokenRegion>();

@@ -229,7 +227,7 @@ namespace DafnyLanguage
         difference = SymmetricDifference(oldSpanCollection, newSpanCollection);

 

         // save the scan result

-        DafnyTokenTagger._scanResult = new ScanResult(_snapshot, snapshot, regions, difference);

+        _buffer.Properties[bufferTokenTaggerKey] = new ScanResult(_snapshot, snapshot, regions, difference);

         // save the new baseline

         _snapshot = snapshot;

         _regions = regions;

@@ -468,11 +466,12 @@ namespace DafnyLanguage
       return new SnapshotPoint(newSnapshot, start + N);

     }

 

-    private static List<TokenRegion> Scan(ITextSnapshot newSnapshot) {

+    private List<TokenRegion> Scan(ITextSnapshot newSnapshot) {      

       List<TokenRegion> newRegions; 

-      if (DafnyTokenTagger._scanResult != null &&

-        DafnyTokenTagger._scanResult._newSnapshot == newSnapshot) {

-        newRegions = DafnyTokenTagger._scanResult._regions;

+      ScanResult result;

+      if (_buffer.Properties.TryGetProperty(bufferTokenTaggerKey, out result) &&         

+        result._newSnapshot == newSnapshot) {

+        newRegions = result._regions;

       } else {

         newRegions = new List<TokenRegion>();

         int nextLineNumber = -1;

@@ -485,7 +484,7 @@ namespace DafnyLanguage
           SnapshotPoint end = Scan(txt, line.Start, newRegions, newSnapshot);

           nextLineNumber = newSnapshot.GetLineFromPosition(end).LineNumber;

         }

-        DafnyTokenTagger._scanResult = new ScanResult(null, newSnapshot, newRegions, null);

+        _buffer.Properties[bufferTokenTaggerKey] = new ScanResult(null, newSnapshot, newRegions, null);

       }

       return newRegions;

     }