summaryrefslogtreecommitdiff
path: root/Util/VS2010
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-17 11:29:05 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-17 11:29:05 -0700
commiteaa507dad5904016694a0b019d1e2b8c6406c1c7 (patch)
tree791be8464f713064af7883d6c10f5f302ec9ef76 /Util/VS2010
parent4c5d48ffa0b0e4328ef333d62d7df51190f17f36 (diff)
DafnyExtension: toward some fixes
Diffstat (limited to 'Util/VS2010')
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs2
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs26
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs28
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs46
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs24
5 files changed, 80 insertions, 46 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index b7b2cd6d..79194d97 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -47,7 +47,7 @@ namespace DafnyLanguage
}
}
- public Dafny.Program Process() {
+ public Dafny.Program ProcessResolution() {
if (!ParseAndTypeCheck()) {
return null;
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index db91cd92..4f414b91 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -89,16 +89,24 @@ namespace DafnyLanguage
void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
var r = sender as ResolverTagger;
- if (r != null && r._program != null) {
- if (!ComputeIdentifierRegions(r._program, r._snapshot))
- return; // no new regions
+ if (r != null) {
+ ITextSnapshot snap;
+ Microsoft.Dafny.Program prog;
+ lock (this) {
+ snap = r._snapshot;
+ prog = r._program;
+ }
+ if (prog != null) {
+ if (!ComputeIdentifierRegions(prog, snap))
+ return; // no new regions
- var chng = TagsChanged;
- if (chng != null) {
- NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);
- if (spans.Count > 0) {
- SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
- chng(this, new SnapshotSpanEventArgs(span));
+ var chng = TagsChanged;
+ if (chng != null) {
+ NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);
+ if (spans.Count > 0) {
+ SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
+ chng(this, new SnapshotSpanEventArgs(span));
+ }
}
}
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
index e51e9887..a47cdba7 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
@@ -91,16 +91,24 @@ namespace DafnyLanguage
void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
var r = sender as ResolverTagger;
- if (r != null && r._program != null) {
- if (!ComputeOutliningRegions(r._program, r._snapshot))
- return; // no new regions
-
- var chng = TagsChanged;
- if (chng != null) {
- NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);
- if (spans.Count > 0) {
- SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
- chng(this, new SnapshotSpanEventArgs(span));
+ if (r != null) {
+ ITextSnapshot snap;
+ Microsoft.Dafny.Program prog;
+ lock (this) {
+ snap = r._snapshot;
+ prog = r._program;
+ }
+ if (prog != null) {
+ if (!ComputeOutliningRegions(prog, snap))
+ return; // no new regions
+
+ var chng = TagsChanged;
+ if (chng != null) {
+ NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);
+ if (spans.Count > 0) {
+ SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
+ chng(this, new SnapshotSpanEventArgs(span));
+ }
}
}
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
index 34dcce3c..d8a60647 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
@@ -121,19 +121,22 @@ namespace DafnyLanguage
// If r._program is null, then the current buffer contains a Dafny fragment that does not resolve. If it is non-null,
// then r._program has been successfully resolved, so when things have been sufficiently idle, we're ready to verify it.
resolver = r;
- latestProgram = r._program;
- latestSnapshot = latestProgram != null ? r._snapshot : null;
+ lock (r) {
+ latestProgram = r._program;
+ latestSnapshot = latestProgram != null ? r._snapshot : null;
+ }
}
}
bool verificationInProgress; // this field is protected by "this"
+ bool verificationRequested; // this field is protected by "this". Invariant: verificationRequested ==> verificationInProgress
public void DoTheVerification(object sender, EventArgs args) {
var buffer = sender as ITextBuffer;
if (buffer != null && latestProgram != null && resolver != null) {
bool tagsChanged = false;
lock (this) {
if (verificationInProgress) {
- // take no further action
+ verificationRequested = true;
return;
}
verificationInProgress = true;
@@ -185,25 +188,30 @@ namespace DafnyLanguage
}
public void Start() {
- var newErrors = new List<DafnyError>();
- bool success = DafnyDriver.Verify(program, errorInfo => {
- newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
- foreach (var aux in errorInfo.Aux) {
- newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
+ bool verifySomeMore = true;
+ while (verifySomeMore) {
+ var newErrors = new List<DafnyError>();
+ bool success = DafnyDriver.Verify(program, errorInfo => {
+ newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
+ foreach (var aux in errorInfo.Aux) {
+ newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
+ }
+ });
+
+ lock (pt) {
+ verifySomeMore = pt.verificationRequested;
+ pt.verificationInProgress = verifySomeMore;
+ pt.verificationRequested = false;
+ if (pt.bufferChangesPreVerificationStart.Count != 0) {
+ pt.bufferChangesPreVerificationStart = new List<SnapshotSpan>();
+ }
+ resolver.PopulateErrorList(newErrors, true, snapshot); // TODO: is this appropriate to do inside the monitor?
}
- });
- lock (pt) {
- pt.verificationInProgress = false;
- if (pt.bufferChangesPreVerificationStart.Count != 0) {
- pt.bufferChangesPreVerificationStart = new List<SnapshotSpan>();
+ var chng = pt.TagsChanged;
+ if (chng != null) {
+ chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
}
- resolver.PopulateErrorList(newErrors, true, snapshot); // TODO: is this appropriate to do inside the monitor?
- }
-
- var chng = pt.TagsChanged;
- if (chng != null) {
- chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
}
}
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
index 2017cfaa..398629ab 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
@@ -70,11 +70,12 @@ namespace DafnyLanguage
{
ITextBuffer _buffer;
ITextDocument _document;
+ // 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
List<DafnyError> _resolutionErrors = new List<DafnyError>(); // if nonempty, then _snapshot is the snapshot from which the errors were produced
List<DafnyError> _verificationErrors = new List<DafnyError>();
ErrorListProvider _errorProvider;
- public Dafny.Program _program; // non-null only if the snapshot contains a Dafny program that type checks
internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) {
_buffer = buffer;
@@ -138,15 +139,22 @@ namespace DafnyLanguage
yield return new TagSpan<DafnyResolverTag>(span, new DafnyErrorResolverTag(ty, err.Message));
}
}
- if (_program != null) {
- yield return new TagSpan<DafnyResolverTag>(new SnapshotSpan(_snapshot, 0, _snapshot.Length), new DafnySuccessResolverTag(_program));
+
+ ITextSnapshot snap;
+ Dafny.Program prog;
+ lock (this) {
+ snap = _snapshot;
+ prog = _program;
+ }
+ if (prog != null) {
+ yield return new TagSpan<DafnyResolverTag>(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog));
}
}
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
/// <summary>
- /// Calls the Dafny verifier on the program, updates the Error List accordingly.
+ /// Calls the Dafny parser/resolver/type checker on the program, updates the Error List accordingly.
/// </summary>
void ProcessFile(object sender, EventArgs args) {
ITextSnapshot snapshot = _buffer.CurrentSnapshot;
@@ -158,7 +166,7 @@ namespace DafnyLanguage
List<DafnyError> newErrors;
Dafny.Program program;
try {
- program = driver.Process();
+ program = driver.ProcessResolution();
newErrors = driver.Errors;
} catch (Exception e) {
newErrors = new List<DafnyError>();
@@ -166,8 +174,10 @@ namespace DafnyLanguage
program = null;
}
- _snapshot = snapshot;
- _program = program;
+ lock (this) {
+ _snapshot = snapshot;
+ _program = program;
+ }
PopulateErrorList(newErrors, false, snapshot);
}