From 10a8896ae40fd918abbb8caa616ac6ee0876ac1d Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 29 May 2015 16:29:15 -0700 Subject: Add an infinite set collection type. --- Source/DafnyExtension/TokenTagger.cs | 1 + 1 file changed, 1 insertion(+) (limited to 'Source/DafnyExtension/TokenTagger.cs') diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index af141ad7..8377b3a2 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -305,6 +305,7 @@ namespace DafnyLanguage case "ghost": case "if": case "imap": + case "iset": case "import": case "in": case "include": -- cgit v1.2.3 From 817d28da901dc8d285c8e7f86f25496093fd6af2 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Wed, 6 Jan 2016 11:49:34 -0800 Subject: Fix some VS IDE performance issues. - cache scan results so it can be shared between different instances of DafnyTokenTagger - Instead of rescanning the whole text buffer upon a text change, only rescan the text span that the text change is in. - set the timer to half a second to match the comment at the beginnig of the file. The event change are only passed along to Dafny when the user stop typing for half a second. - Change framework dependence so the project can work with version 4.5 and higher. --- Source/DafnyExtension/BufferIdleEventUtil.cs | 2 +- Source/DafnyExtension/TokenTagger.cs | 214 ++++++++++++++++----- .../DafnyExtension/source.extension.vsixmanifest | 2 +- 3 files changed, 168 insertions(+), 50 deletions(-) (limited to 'Source/DafnyExtension/TokenTagger.cs') diff --git a/Source/DafnyExtension/BufferIdleEventUtil.cs b/Source/DafnyExtension/BufferIdleEventUtil.cs index 5ab9df09..8a1ad0ed 100644 --- a/Source/DafnyExtension/BufferIdleEventUtil.cs +++ b/Source/DafnyExtension/BufferIdleEventUtil.cs @@ -120,7 +120,7 @@ namespace DafnyLanguage { timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle) { - Interval = TimeSpan.FromMilliseconds(50) + Interval = TimeSpan.FromMilliseconds(500) }; timer.Tick += (s, e) => diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index 8377b3a2..f1c4860c 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -70,17 +70,37 @@ namespace DafnyLanguage } } + internal sealed class DafnyTokenTagger : ITagger, IDisposable { + internal sealed class ScanResult + { + internal ITextSnapshot _oldSnapshot; + internal ITextSnapshot _newSnapshot; + internal List _regions; // the regions computed for the _newSnapshot + internal NormalizedSnapshotSpanCollection _difference; // the difference between _oldSnapshot and _newSnapshot + + internal ScanResult(ITextSnapshot oldSnapshot, ITextSnapshot newSnapshot, List regions, NormalizedSnapshotSpanCollection diffs) { + _oldSnapshot = oldSnapshot; + _newSnapshot = newSnapshot; + _regions = regions; + _difference = diffs; + } + } + 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; bool _disposed; internal DafnyTokenTagger(ITextBuffer buffer) { _buffer = buffer; _snapshot = buffer.CurrentSnapshot; - _regions = Rescan(_snapshot); + _regions = Scan(_snapshot); _buffer.Changed += new EventHandler(ReparseFile); } @@ -92,6 +112,7 @@ namespace DafnyLanguage _buffer = null; _snapshot = null; _regions = null; + _scanResult = null; _disposed = true; } } @@ -127,24 +148,92 @@ namespace DafnyLanguage ITextSnapshot snapshot = _buffer.CurrentSnapshot; if (snapshot == _snapshot) 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; + // save the new baseline + _regions = DafnyTokenTagger._scanResult._regions; + _snapshot = snapshot; + } else { + List regions = new List(); + List rescannedRegions = new List(); + + // loop through the changes and check for changes in comments first. If + // the change is in a comments, we need to rescan starting from the + // beginning of the comments (which in multi-lined comments, it can + // be a line that the changes are not on), otherwise, we can just rescan the lines + // that the changes are on. + bool done; + SnapshotPoint start, end; + for (int i = 0; i < args.Changes.Count; i++) { + done = false; + // get the span of the lines that the change is on. + int cStart = args.Changes[i].NewSpan.Start; + int cEnd = args.Changes[i].NewSpan.End; + start = snapshot.GetLineFromPosition(cStart).Start; + end = snapshot.GetLineFromPosition(cEnd).End; + SnapshotSpan newSpan = new SnapshotSpan(start, end); + foreach (TokenRegion r in _regions) { + if (r.Kind == DafnyTokenKind.Comment) { + // if the change is in the comments, we want to start scanning from the + // the beginning of the comments instead. + SnapshotSpan span = r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive); + if (span.IntersectsWith(newSpan)) { + start = span.Start.Position < newSpan.Start.Position ? span.Start : newSpan.Start; + end = span.End.Position > newSpan.End.Position ? span.End : newSpan.End; + end = Scan(snapshot.GetText(new SnapshotSpan(start, end)), start, regions, snapshot); + // record the regions that we rescanned. + rescannedRegions.Add(new SnapshotSpan(start, end)); + done = true; + break; + } + } + } + if (!done) { + // scan the lines that the change is on to generate the new regions. + end = Scan(snapshot.GetText(new SnapshotSpan(start, end)), start, regions, snapshot); + // record the span that we rescanned. + rescannedRegions.Add(new SnapshotSpan(start, end)); + } + } - // get all of the outline regions in the snapshot - List newRegions = Rescan(snapshot); - - // determine the changed span, and send a changed event with the new spans - List oldSpans = new List(_regions.Select(r => - r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive))); - - List newSpans = new List(newRegions.Select(r => r.Span)); - - NormalizedSnapshotSpanCollection oldSpanCollection = new NormalizedSnapshotSpanCollection(oldSpans); - NormalizedSnapshotSpanCollection newSpanCollection = new NormalizedSnapshotSpanCollection(newSpans); - - NormalizedSnapshotSpanCollection difference = SymmetricDifference(oldSpanCollection, newSpanCollection); - - // save the new baseline - _snapshot = snapshot; - _regions = newRegions; + List oldSpans = new List(); + List newSpans = new List(); + // record the newly created spans. + foreach (TokenRegion r in regions) { + newSpans.Add(r.Span); + } + // loop through the old scan results and remove the ones that + // are in the regions that are rescanned. + foreach (TokenRegion r in _regions) { + SnapshotSpan origSpan = r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive); + bool obsolete = false; + foreach (SnapshotSpan span in rescannedRegions) { + if (origSpan.IntersectsWith(span)) { + oldSpans.Add(span); + obsolete = true; + break; + } + } + if (!obsolete) { + TokenRegion region = new TokenRegion(origSpan.Start, origSpan.End, r.Kind); + regions.Add(region); + } + } + + NormalizedSnapshotSpanCollection oldSpanCollection = new NormalizedSnapshotSpanCollection(oldSpans); + NormalizedSnapshotSpanCollection newSpanCollection = new NormalizedSnapshotSpanCollection(newSpans); + difference = SymmetricDifference(oldSpanCollection, newSpanCollection); + + // save the scan result + DafnyTokenTagger._scanResult = new ScanResult(_snapshot, snapshot, regions, difference); + // save the new baseline + _snapshot = snapshot; + _regions = regions; + } var chng = TagsChanged; if (chng != null) { @@ -160,38 +249,35 @@ namespace DafnyLanguage NormalizedSnapshotSpanCollection.Difference(second, first)); } - private static List Rescan(ITextSnapshot newSnapshot) { - List newRegions = new List(); - + private static SnapshotPoint Scan(string txt, SnapshotPoint start, List newRegions, ITextSnapshot newSnapshot) { int longCommentDepth = 0; - SnapshotPoint commentStart = new SnapshotPoint(); // used only when longCommentDepth != 0 + SnapshotPoint commentStart = new SnapshotPoint(); SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint(); // used only when longCommentDepth != 0 - foreach (ITextSnapshotLine line in newSnapshot.Lines) { - string txt = line.GetText(); // the current line (without linebreak characters) - int N = txt.Length; // length of the current line - int cur = 0; // offset into the current line - + int N = txt.Length; + bool done = false; + while (!done) { + N = txt.Length; // length of the current buffer + int cur = 0; // offset into the current buffer if (longCommentDepth != 0) { ScanForEndOfComment(txt, ref longCommentDepth, ref cur); if (longCommentDepth == 0) { // we just finished parsing a long comment - newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKind.Comment)); + newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, start + cur), DafnyTokenKind.Comment)); } else { // we're still parsing the long comment Contract.Assert(cur == txt.Length); - commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + cur); + commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, start + cur); goto OUTER_CONTINUE; } } - - // repeatedly get the remaining tokens from this line - int end; // offset into the current line + // repeatedly get the remaining tokens from this buffer + int end; // offset into the current buffer for (; ; cur = end) { // advance to the first character of a keyword or token DafnyTokenKind ty = DafnyTokenKind.Keyword; for (; ; cur++) { if (N <= cur) { - // we've looked at everything in this line + // we've looked at everything in this buffer goto OUTER_CONTINUE; } char ch = txt[cur]; @@ -204,7 +290,7 @@ namespace DafnyLanguage } // advance to the end of the token - end = cur + 1; // offset into the current line + end = cur + 1; // offset into the current buffer if (ty == DafnyTokenKind.Number) { // scan the rest of this number for (; end < N; end++) { @@ -213,7 +299,7 @@ namespace DafnyLanguage } else break; } } else if (ty == DafnyTokenKind.String) { - // scan the rest of this string, but not past the end-of-line + // scan the rest of this string, but not past the end-of-buffer for (; end < N; end++) { char ch = txt[end]; if (ch == '"') { @@ -233,20 +319,20 @@ namespace DafnyLanguage if (end == N) continue; // this was not the start of a comment; it was just a single "/" and we don't care to color it char ch = txt[end]; if (ch == '/') { - // a short comment - end = N; + // a short comment, to the end of the line. + end = newSnapshot.GetLineFromPosition(start + end).End.Position - start; } else if (ch == '*') { // a long comment; find the matching "*/" end++; - commentStart = new SnapshotPoint(newSnapshot, line.Start + cur); + commentStart = new SnapshotPoint(newSnapshot, start + cur); Contract.Assert(longCommentDepth == 0); longCommentDepth = 1; ScanForEndOfComment(txt, ref longCommentDepth, ref end); if (longCommentDepth == 0) { // we finished scanning a long comment, and "end" is set to right after it - newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKind.Comment)); + newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, start + end), DafnyTokenKind.Comment)); } else { - commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + end); + commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, start + end); } continue; } else { @@ -358,21 +444,53 @@ namespace DafnyLanguage } } } - - newRegions.Add(new TokenRegion(new SnapshotPoint(newSnapshot, line.Start + cur), new SnapshotPoint(newSnapshot, line.Start + end), ty)); + newRegions.Add(new TokenRegion(new SnapshotPoint(newSnapshot, start + cur), new SnapshotPoint(newSnapshot, start + end), ty)); + } + OUTER_CONTINUE: + done = true; + if (longCommentDepth != 0) { + // we need to look into the next line + ITextSnapshotLine currLine = newSnapshot.GetLineFromPosition(start + N); + if ((currLine.LineNumber + 1) < newSnapshot.LineCount) { + ITextSnapshotLine nextLine = newSnapshot.GetLineFromLineNumber(currLine.LineNumber + 1); + txt = nextLine.GetText(); + start = nextLine.Start; + // we are done scanning the current buffer, but not the whole file yet. + // we need to continue to find the enclosing "*/", or until the end of the file. + done = false; + } else { + // This was a malformed comment, running to the end of the buffer. Above, we let "commentEndAsWeKnowIt" be the end of the + // last line, so we can use it here. + newRegions.Add(new TokenRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKind.Comment)); + } } - OUTER_CONTINUE: ; } + return new SnapshotPoint(newSnapshot, start + N); + } - if (longCommentDepth != 0) { - // This was a malformed comment, running to the end of the buffer. Above, we let "commentEndAsWeKnowIt" be the end of the - // last line, so we can use it here. - newRegions.Add(new TokenRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKind.Comment)); + private static List Scan(ITextSnapshot newSnapshot) { + List newRegions; + if (DafnyTokenTagger._scanResult != null && + DafnyTokenTagger._scanResult._newSnapshot == newSnapshot) { + newRegions = DafnyTokenTagger._scanResult._regions; + } else { + newRegions = new List(); + int nextLineNumber = -1; + foreach (ITextSnapshotLine line in newSnapshot.Lines) { + if (line.LineNumber <= nextLineNumber) { + // the line is already processed. + continue; + } + string txt = line.GetText(); // the current line (without linebreak characters) + SnapshotPoint end = Scan(txt, line.Start, newRegions, newSnapshot); + nextLineNumber = newSnapshot.GetLineFromPosition(end).LineNumber; + } + DafnyTokenTagger._scanResult = new ScanResult(null, newSnapshot, newRegions, null); } - return newRegions; } + /// /// Scans "txt" beginning with depth "depth", which is assumed to be non-0. Any occurrences of "/*" or "*/" /// increment or decrement "depth". If "depth" ever reaches 0, then "end" returns as the number of characters diff --git a/Source/DafnyExtension/source.extension.vsixmanifest b/Source/DafnyExtension/source.extension.vsixmanifest index 66e4deda..a3987456 100644 --- a/Source/DafnyExtension/source.extension.vsixmanifest +++ b/Source/DafnyExtension/source.extension.vsixmanifest @@ -11,7 +11,7 @@ - + -- cgit v1.2.3 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(-) (limited to 'Source/DafnyExtension/TokenTagger.cs') 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