From 3c572baf712bccd21572a17866c8bb46b47c4064 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Tue, 2 Jul 2013 18:59:10 -0700
Subject: DafnyExtension: Enabled verification result caching by default.

---
 Source/DafnyExtension/ProgressMargin.cs | 14 ++++++++++----
 Source/DafnyMenu/DafnyMenu.vsct         |  2 +-
 Source/DafnyMenu/DafnyMenuPackage.cs    |  1 +
 3 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 4a5553dc..e481f141 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -132,6 +132,7 @@ namespace DafnyLanguage
         {
           _buffer.Changed -= buffer_Changed;
           _errorProvider.Dispose();
+          ClearCachedVerificationResults();
           if (resolver != null)
           {
             resolver.Dispose();
@@ -286,14 +287,19 @@ namespace DafnyLanguage
         bufferChangesPostVerificationStart.Clear();
         bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));
         verificationDisabled = false;
-        if (_document != null)
-        {
-          Microsoft.Boogie.ExecutionEngine.Cache.RemoveMatchingKeys(new Regex(string.Format(@"^{0}", Regex.Escape(GetHashCode().ToString()))));
-        }
+        ClearCachedVerificationResults();
         NotifyAboutChangedTags(_buffer.CurrentSnapshot);
       }
     }
 
+    private void ClearCachedVerificationResults()
+    {
+      if (_document != null)
+      {
+        Microsoft.Boogie.ExecutionEngine.Cache.RemoveMatchingKeys(new Regex(string.Format(@"^{0}:", Regex.Escape(GetHashCode().ToString()))));
+      }
+    }
+
     /// <summary>
     /// Thread entry point.
     /// </summary>
diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index c4f562e4..5cb2975d 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -99,7 +99,7 @@
         <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
         <CommandFlag>TextChanges</CommandFlag>
         <Strings>
-          <ButtonText>Enable on-demand re-verification</ButtonText>
+          <ButtonText>Disable on-demand re-verification</ButtonText>
         </Strings>
       </Button>
 
diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 9bef8d88..294b0b75 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -88,6 +88,7 @@ namespace DafnyLanguage.DafnyMenu
         mcs.AddCommand(stopVerifierCommand);
 
         var toggleSnapshotVerificationCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleSnapshotVerification);
+        DafnyDriver.ToggleIncrementalVerification();
         toggleSnapshotVerificationCommand = new OleMenuCommand(ToggleSnapshotVerificationCallback, toggleSnapshotVerificationCommandID);
         mcs.AddCommand(toggleSnapshotVerificationCommand);
 
-- 
cgit v1.2.3