diff options
| author |  wuestholz <unknown> | 2013-05-27 14:44:45 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-05-27 14:44:45 -0700 |
| commit | 424c8820500e281b9eca07322183877601de7562 (patch) | |
| tree | c3f1d52e3e8d67ed9bcf6b3d85af7001d257bd25 | |
| parent | ef3ccef52b432a7d5c8c7db2add8102bd281b58c (diff) | |
DafnyExtension: Fixed an issue (error list wasn't cleared after closing buffers).
| -rw-r--r-- | Source/DafnyExtension/ProgressMargin.cs | 25 | ||||
| -rw-r--r-- | Source/DafnyExtension/ResolverTagger.cs | 36 |
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.
|