summaryrefslogtreecommitdiff
path: root/Util
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-08-27 17:41:34 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-08-27 17:41:34 -0700
commit5732d706a756dd16ac2acc9f456f34ddab94bde6 (patch)
treeecd14c67a6c05d8bb59ad65ab9126e1da134a321 /Util
parent1608c9def153fd9199d1a0e7192c5dd42f20eab8 (diff)
DafnyExtension: don't reverify a buffer with no changes
Diffstat (limited to 'Util')
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs5
1 files changed, 4 insertions, 1 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
index 33f00ab2..286047ec 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
@@ -157,7 +157,10 @@ namespace DafnyLanguage
// We have a successfully resolved program to verify
var resolvedVersion = snap.Version.VersionNumber;
- if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion)) {
+ if (bufferChangesPostVerificationStart.Count == 0) {
+ // Nothing new to verify. No reason to start a new verification.
+ return;
+ } else if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion)) {
// There have been buffer changes since the program that was resolved. Do nothing here,
// and instead just await the next resolved program.
return;