DafnyExtension: Added a menu item to toggle verification result caching.

3 files changed, 21 insertions, 0 deletions

diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 812a06e8..c4f562e4 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -95,6 +95,14 @@
         </Strings>

       </Button>

 

+      <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleSnapshotVerification" priority="0x0103" type="Button">

+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />

+        <CommandFlag>TextChanges</CommandFlag>

+        <Strings>

+          <ButtonText>Enable on-demand re-verification</ButtonText>

+        </Strings>

+      </Button>

+

     </Buttons>

 

     <!--The bitmaps section is used to define the bitmaps that are used for the commands.-->

@@ -124,6 +132,7 @@
       <IDSymbol name="cmdidCompile" value="0x0100" />

       <IDSymbol name="cmdidRunVerifier" value="0x0101" />

       <IDSymbol name="cmdidStopVerifier" value="0x0102" />

+      <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />

     </GuidSymbol>

 

     <!--

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 54f3a4dd..9bef8d88 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -38,6 +38,7 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand menuCommand;

     private OleMenuCommand runVerifierCommand;

     private OleMenuCommand stopVerifierCommand;

+    private OleMenuCommand toggleSnapshotVerificationCommand;

 

     /// <summary>

     /// Default constructor of the package.

@@ -86,6 +87,10 @@ namespace DafnyLanguage.DafnyMenu
         stopVerifierCommand.BeforeQueryStatus += stopVerifierCommand_BeforeQueryStatus;

         mcs.AddCommand(stopVerifierCommand);

 

+        var toggleSnapshotVerificationCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleSnapshotVerification);

+        toggleSnapshotVerificationCommand = new OleMenuCommand(ToggleSnapshotVerificationCallback, toggleSnapshotVerificationCommandID);

+        mcs.AddCommand(toggleSnapshotVerificationCommand);

+

         var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);

         menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);

         menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;

@@ -94,6 +99,12 @@ namespace DafnyLanguage.DafnyMenu
       }

     }

 

+    private void ToggleSnapshotVerificationCallback(object sender, EventArgs e)

+    {

+      var on = DafnyDriver.ToggleIncrementalVerification();

+      toggleSnapshotVerificationCommand.Text = (on ? "Disable" : "Enable") + " on-demand re-verification";

+    }

+

     private void StopVerifierCallback(object sender, EventArgs e)

     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index 5f0213cc..0cf3869e 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -10,5 +10,6 @@ namespace DafnyLanguage.DafnyMenu
     public const uint cmdidRunVerifier = 0x101;

     public const uint cmdidStopVerifier = 0x102;

     public const uint cmdidMenu = 0x1021;

+    public static int cmdidToggleSnapshotVerification = 0x103;

   };

 }
\ No newline at end of file