From ff6013dc188625ba11832b56138722161e3bb5d0 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 20 Jun 2014 18:03:31 +0200
Subject: DafnyExtension: Minor change to deal with a change in the Boogie
 command-line options

---
 Source/DafnyExtension/DafnyDriver.cs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 801e3ebd..f4eb4fb7 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -217,8 +217,9 @@ namespace DafnyLanguage
 
     public static bool ToggleIncrementalVerification()
     {
-      Dafny.DafnyOptions.Clo.VerifySnapshots = !Dafny.DafnyOptions.Clo.VerifySnapshots;
-      return Dafny.DafnyOptions.Clo.VerifySnapshots;
+      // TODO(wuestholz): Change this once there are more than two options.
+      Dafny.DafnyOptions.Clo.VerifySnapshots = (Dafny.DafnyOptions.Clo.VerifySnapshots + 1) % 2;
+      return 0 < Dafny.DafnyOptions.Clo.VerifySnapshots;
     }
 
     public static bool Verify(Dafny.Program dafnyProgram, ResolverTagger resolver, string uniqueIdPrefix, string requestId, ErrorReporterDelegate er) {
-- 
cgit v1.2.3


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/DafnyExtension/DafnyDriver.cs | 29 +++++++++++++++++++++-----
 Source/DafnyExtension/MenuProxy.cs   | 15 ++++++++++++--
 Source/DafnyMenu/DafnyMenu.vsct      | 11 ++++++++++
 Source/DafnyMenu/DafnyMenuPackage.cs | 40 +++++++++++++++++++++++++++++++++---
 Source/DafnyMenu/PkgCmdID.cs         |  1 +
 5 files changed, 86 insertions(+), 10 deletions(-)

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index f4eb4fb7..36b07d60 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -45,7 +45,7 @@ namespace DafnyLanguage
 
         ExecutionEngine.printer = new DummyPrinter();
         ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();
-        ToggleIncrementalVerification();
+        ChangeIncrementalVerification(1);
       }
     }
 
@@ -215,11 +215,30 @@ namespace DafnyLanguage
       }
     }
 
-    public static bool ToggleIncrementalVerification()
+    public static int IncrementalVerificationMode()
     {
-      // TODO(wuestholz): Change this once there are more than two options.
-      Dafny.DafnyOptions.Clo.VerifySnapshots = (Dafny.DafnyOptions.Clo.VerifySnapshots + 1) % 2;
-      return 0 < Dafny.DafnyOptions.Clo.VerifySnapshots;
+      return Dafny.DafnyOptions.Clo.VerifySnapshots;
+    }
+
+    public static int ChangeIncrementalVerification(int mode)
+    {
+      var old = Dafny.DafnyOptions.Clo.VerifySnapshots;
+      if (mode == 1 && old != 0)
+      {
+        // Disable mode 1.
+        Dafny.DafnyOptions.Clo.VerifySnapshots = 0;
+      }
+      else if (mode == 2 && old == 2)
+      {
+        // Disable mode 2.
+        Dafny.DafnyOptions.Clo.VerifySnapshots = 1;
+      }
+      else
+      {
+        // Enable mode.
+        Dafny.DafnyOptions.Clo.VerifySnapshots = mode;
+      }
+      return Dafny.DafnyOptions.Clo.VerifySnapshots;
     }
 
     public static bool Verify(Dafny.Program dafnyProgram, ResolverTagger resolver, string uniqueIdPrefix, string requestId, ErrorReporterDelegate er) {
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index a67ba602..11e1287f 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -17,9 +17,20 @@ namespace DafnyLanguage
       this.DafnyMenuPackage = DafnyMenuPackage;
     }
 
-    public bool ToggleSnapshotVerification(IWpfTextView activeTextView)
+    public int ToggleSnapshotVerification(IWpfTextView activeTextView)
     {
-      return DafnyDriver.ToggleIncrementalVerification();
+      return DafnyDriver.ChangeIncrementalVerification(1);
+    }
+
+    public int ToggleMoreAdvancedSnapshotVerification(IWpfTextView activeTextView)
+    {
+      return DafnyDriver.ChangeIncrementalVerification(2);
+    }
+
+    public bool MoreAdvancedSnapshotVerificationCommandEnabled(IWpfTextView activeTextView)
+    {
+      return activeTextView != null
+             && 0 < DafnyDriver.IncrementalVerificationMode();
     }
 
     public bool StopVerifierCommandEnabled(IWpfTextView activeTextView)
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