DafnyExtension: Made it possible to activate the more advanced verification result caching in Boogie (experimental for now).

3 files changed, 49 insertions, 3 deletions

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