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

1 files changed, 11 insertions, 0 deletions

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;