summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs38
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)