summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-05-27 14:44:45 -0700
committerGravatar wuestholz <unknown>2013-05-27 14:44:45 -0700
commit424c8820500e281b9eca07322183877601de7562 (patch)
treec3f1d52e3e8d67ed9bcf6b3d85af7001d257bd25
parentef3ccef52b432a7d5c8c7db2add8102bd281b58c (diff)
DafnyExtension: Fixed an issue (error list wasn't cleared after closing buffers).
-rw-r--r--Source/DafnyExtension/ProgressMargin.cs25
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs36
2 files changed, 51 insertions, 10 deletions
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index edaa5019..f5faf697 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -110,8 +110,28 @@ namespace DafnyLanguage
bufferChangesPostVerificationStart.Add(new SnapshotSpan(buffer.CurrentSnapshot, 0, buffer.CurrentSnapshot.Length));
}
- public void Dispose() {
- _errorProvider.Dispose();
+ public void Dispose()
+ {
+ Dispose(true);
+ GC.SuppressFinalize(this);
+ }
+
+ private void Dispose(bool disposing)
+ {
+ if (!m_disposed)
+ {
+ if (disposing)
+ {
+ _buffer.Changed -= buffer_Changed;
+ _errorProvider.Dispose();
+ if (resolver != null)
+ {
+ resolver.Dispose();
+ }
+ }
+
+ m_disposed = true;
+ }
}
// The following fields and the contents of the following two lists are protected by the lock "this".
@@ -280,6 +300,7 @@ namespace DafnyLanguage
}
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+ private bool m_disposed;
IEnumerable<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans) {
if (spans.Count == 0) yield break;
var targetSnapshot = spans[0].Snapshot;
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 81efe28a..4f8fa694 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -90,16 +90,35 @@ namespace DafnyLanguage
BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer);
}
- public void Dispose() {
- if (_errorProvider != null) {
- try {
- _errorProvider.Tasks.Clear();
- } catch (InvalidOperationException) {
- // this may occur if the SVsServiceProvider somehow has been uninstalled before our Dispose method is called
+ public void Dispose()
+ {
+ Dispose(true);
+ GC.SuppressFinalize(this);
+ }
+
+ private void Dispose(bool disposing)
+ {
+ if (!m_disposed)
+ {
+ if (disposing)
+ {
+ if (_errorProvider != null)
+ {
+ try
+ {
+ _errorProvider.Tasks.Clear();
+ }
+ catch (InvalidOperationException)
+ {
+ // this may occur if the SVsServiceProvider somehow has been uninstalled before our Dispose method is called
+ }
+ _errorProvider.Dispose();
+ }
+ BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);
}
- _errorProvider.Dispose();
+
+ m_disposed = true;
}
- BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);
}
public IEnumerable<DafnyError> AllErrors() {
@@ -155,6 +174,7 @@ namespace DafnyLanguage
}
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+ private bool m_disposed;
/// <summary>
/// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly.