DafnyExtension: Enabled verification result caching by default.

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);