From 0a3b095205a91b480a0b89c404981c498f088747 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 12 Jun 2013 16:40:09 -0700
Subject: DafnyExtension: Added a menu item to toggle verification result
 caching.

---
 Source/DafnyMenu/DafnyMenu.vsct      |  9 +++++++++
 Source/DafnyMenu/DafnyMenuPackage.cs | 11 +++++++++++
 Source/DafnyMenu/PkgCmdID.cs         |  1 +
 3 files changed, 21 insertions(+)

(limited to 'Source/DafnyMenu')

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
-- 
cgit v1.2.3