diff options
| author |  wuestholz <unknown> | 2013-07-10 18:21:14 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-10 18:21:14 -0700 |
| commit | 5df8661c279d98990c2852f559d8b67fa9b0c92e (patch) | |
| tree | ed4a19290ebdbf1a9977cc05fb6e6d0e7bbe2e1d /Source/DafnyExtension/ResolverTagger.cs | |
| parent | 8e467cdab8f3de3933a0cfbe372520225adcc97d (diff) | |
Did some refactoring of the interaction with the Boogie execution engine.
Diffstat (limited to 'Source/DafnyExtension/ResolverTagger.cs')
| -rw-r--r-- | Source/DafnyExtension/ResolverTagger.cs | 54 |
1 files changed, 29 insertions, 25 deletions
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs index 33baf3b5..578b9ce2 100644 --- a/Source/DafnyExtension/ResolverTagger.cs +++ b/Source/DafnyExtension/ResolverTagger.cs @@ -87,7 +87,7 @@ namespace DafnyLanguage {
readonly ITextBuffer _buffer;
readonly ITextDocument _document;
- readonly ErrorListProvider _errorProvider;
+ ErrorListProvider _errorProvider;
// The 'Snapshot' and 'Program' fields should be updated and read together, so they are protected by "this"
public ITextSnapshot Snapshot; // may be null
@@ -207,6 +207,7 @@ namespace DafnyLanguage // this may occur if the SVsServiceProvider somehow has been uninstalled before our Dispose method is called
}
_errorProvider.Dispose();
+ _errorProvider = null;
}
BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);
}
@@ -307,35 +308,38 @@ namespace DafnyLanguage public void UpdateErrorList(ITextSnapshot snapshot)
{
- lock (this)
+ lock (this)
{
- _errorProvider.SuspendRefresh(); // reduce flickering
- _errorProvider.Tasks.Clear();
- foreach (var err in AllErrors)
+ if (_errorProvider != null)
{
- var span = err.Span.GetSpan(snapshot);
- var lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);
- var line = snapshot.GetLineFromPosition(span.Start.Position);
- var columnNum = span.Start - line.Start;
- ErrorTask task = new ErrorTask()
- {
- Category = TaskCategory.BuildCompile,
- ErrorCategory = CategoryConversion(err.Category),
- Text = err.Message,
- Line = lineNum,
- Column = columnNum
- };
- if (_document != null)
+ _errorProvider.SuspendRefresh(); // reduce flickering
+ _errorProvider.Tasks.Clear();
+ foreach (var err in AllErrors)
{
- task.Document = _document.FilePath;
- }
- if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)
- {
- task.Navigate += new EventHandler(NavigateHandler);
+ var span = err.Span.GetSpan(snapshot);
+ var lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);
+ var line = snapshot.GetLineFromPosition(span.Start.Position);
+ var columnNum = span.Start - line.Start;
+ ErrorTask task = new ErrorTask()
+ {
+ Category = TaskCategory.BuildCompile,
+ ErrorCategory = CategoryConversion(err.Category),
+ Text = err.Message,
+ Line = lineNum,
+ Column = columnNum
+ };
+ if (_document != null)
+ {
+ task.Document = _document.FilePath;
+ }
+ if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)
+ {
+ task.Navigate += new EventHandler(NavigateHandler);
+ }
+ _errorProvider.Tasks.Add(task);
}
- _errorProvider.Tasks.Add(task);
+ _errorProvider.ResumeRefresh();
}
- _errorProvider.ResumeRefresh();
}
var chng = TagsChanged;
if (chng != null)
|