From e7fb24bc6fb8f4a1a76055a539e15aee52191b35 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 23 Jun 2014 23:37:09 +0200
Subject: DafnyExtension: Made it possible to activate the more advanced
 verification result caching in Boogie (experimental for now).

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

(limited to 'Source/DafnyMenu')

diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 0e8c7855..813ccd23 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -103,6 +103,16 @@
         </Strings>
       </Button>
 
+      <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleMoreAdvancedSnapshotVerification" priority="0x0105" type="Button">
+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
+        <CommandFlag>DefaultInvisible</CommandFlag>
+        <CommandFlag>DynamicVisibility</CommandFlag>
+        <CommandFlag>TextChanges</CommandFlag>
+        <Strings>
+          <ButtonText>Enable more advanced on-demand re-verification</ButtonText>
+        </Strings>
+      </Button>
+
       <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleBVD" priority="0x010a" type="Button">
         <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
         <CommandFlag>DynamicVisibility</CommandFlag>
@@ -144,6 +154,7 @@
       <IDSymbol name="cmdidStopVerifier" value="0x0102" />
       <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />
       <IDSymbol name="cmdidToggleBVD" value="0x0104" />
+      <IDSymbol name="cmdidToggleMoreAdvancedSnapshotVerification" value="0x0105" />
     </GuidSymbol>
 
     <!--
diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 114ddf10..58bf2a26 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -19,7 +19,13 @@ namespace DafnyLanguage.DafnyMenu
 
   public interface IMenuProxy
   {
-    bool ToggleSnapshotVerification(IWpfTextView activeTextView);
+    int ToggleSnapshotVerification(IWpfTextView activeTextView);
+
+
+    int ToggleMoreAdvancedSnapshotVerification(IWpfTextView activeTextView);
+
+
+    bool MoreAdvancedSnapshotVerificationCommandEnabled(IWpfTextView activeTextView);
 
 
     bool StopVerifierCommandEnabled(IWpfTextView activeTextView);
@@ -80,6 +86,7 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand runVerifierCommand;
     private OleMenuCommand stopVerifierCommand;
     private OleMenuCommand toggleSnapshotVerificationCommand;
+    private OleMenuCommand toggleMoreAdvancedSnapshotVerificationCommand;
     private OleMenuCommand toggleBVDCommand;
 
     bool BVDDisabled;
@@ -138,6 +145,11 @@ namespace DafnyLanguage.DafnyMenu
         toggleSnapshotVerificationCommand = new OleMenuCommand(ToggleSnapshotVerificationCallback, toggleSnapshotVerificationCommandID);
         mcs.AddCommand(toggleSnapshotVerificationCommand);
 
+        var toggleMoreAdvancedSnapshotVerificationCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleMoreAdvancedSnapshotVerification);
+        toggleMoreAdvancedSnapshotVerificationCommand = new OleMenuCommand(ToggleMoreAdvancedSnapshotVerificationCallback, toggleMoreAdvancedSnapshotVerificationCommandID);
+        toggleMoreAdvancedSnapshotVerificationCommand.BeforeQueryStatus += toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus;
+        mcs.AddCommand(toggleMoreAdvancedSnapshotVerificationCommand);
+
         var showErrorModelCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleBVD);
         toggleBVDCommand = new OleMenuCommand(ToggleBVDCallback, showErrorModelCommandID);
         toggleBVDCommand.Enabled = true;
@@ -191,8 +203,20 @@ namespace DafnyLanguage.DafnyMenu
       var atv = ActiveTextView;
       if (MenuProxy != null && atv != null)
       {
-        var on = MenuProxy.ToggleSnapshotVerification(atv);
-        toggleSnapshotVerificationCommand.Text = (on ? "Disable" : "Enable") + " on-demand re-verification";
+        var mode = MenuProxy.ToggleSnapshotVerification(atv);
+        toggleSnapshotVerificationCommand.Text = (mode == 1 ? "Disable" : "Enable") + " on-demand re-verification";
+        toggleMoreAdvancedSnapshotVerificationCommand.Text = (mode == 2 ? "Disable" : "Enable") + " more advanced on-demand re-verification";
+      }
+    }
+
+    void ToggleMoreAdvancedSnapshotVerificationCallback(object sender, EventArgs e)
+    {
+      var atv = ActiveTextView;
+      if (MenuProxy != null && atv != null)
+      {
+        var mode = MenuProxy.ToggleMoreAdvancedSnapshotVerification(atv);
+        toggleSnapshotVerificationCommand.Text = (mode != 0 ? "Disable" : "Enable") + " on-demand re-verification";
+        toggleMoreAdvancedSnapshotVerificationCommand.Text = (mode == 2 ? "Disable" : "Enable") + " more advanced on-demand re-verification";
       }
     }
 
@@ -276,6 +300,16 @@ namespace DafnyLanguage.DafnyMenu
       }
     }
 
+    private void toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus(object sender, EventArgs e)
+    {
+      var atv = ActiveTextView;
+      if (MenuProxy != null && atv != null)
+      {
+        var visible = MenuProxy.MoreAdvancedSnapshotVerificationCommandEnabled(atv);
+        toggleMoreAdvancedSnapshotVerificationCommand.Visible = visible;
+      }
+    }
+
     void ToggleBVDCallback(object sender, EventArgs e)
     {
       BVDDisabled = !BVDDisabled;
diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index f3452cb9..b6f30145 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -12,5 +12,6 @@ namespace DafnyLanguage.DafnyMenu
     public const uint cmdidMenu = 0x1021;
     public static uint cmdidToggleSnapshotVerification = 0x103;
     public const uint cmdidToggleBVD = 0x104;
+    public static uint cmdidToggleMoreAdvancedSnapshotVerification = 0x105;
   };
 }
\ No newline at end of file
-- 
cgit v1.2.3