From 8f244896640bae196070aa8b2bfe0b2f0be24e2a Mon Sep 17 00:00:00 2001 From: qunyanm Date: Wed, 20 Jan 2016 16:25:46 -0800 Subject: 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. --- Source/DafnyExtension/DafnyDriver.cs | 49 +++++++++++++++++++++++---------- Source/DafnyExtension/ResolverTagger.cs | 37 +++++++++++++++++++++---- Source/DafnyExtension/TokenTagger.cs | 31 ++++++++++----------- 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 _errors = new List(); public List 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> 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(), 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(), parseErrors); + + if (errorCount != 0 || errString != null) { + runResolver = false; + program = null; + } else { + program = new Dafny.Program(_filename, module, builtIns, errorReporter); + } + _buffer.Properties[bufferDafnyKey] = new Tuple>(_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 /// 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 : ""; - var driver = new DafnyDriver(snapshot, filename); + var driver = new DafnyDriver(_buffer, filename); List 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 _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 regions = new List(); @@ -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 Scan(ITextSnapshot newSnapshot) { + private List Scan(ITextSnapshot newSnapshot) { List 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(); 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; } -- cgit v1.2.3