DafnyExtension: Make it possible to enable and disable BVD.

3 files changed, 33 insertions, 29 deletions

diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index d23ebc7f..0e8c7855 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -103,12 +103,13 @@
         </Strings>

       </Button>

 

-      <Button guid="guidDafnyMenuCmdSet" id="cmdidShowErrorModel" priority="0x010a" type="Button">

+      <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleBVD" priority="0x010a" type="Button">

         <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />

         <CommandFlag>DynamicVisibility</CommandFlag>

         <CommandFlag>DefaultInvisible</CommandFlag>

+        <CommandFlag>TextChanges</CommandFlag>

         <Strings>

-          <ButtonText>Show model for selected error in BVD</ButtonText>

+          <ButtonText>Disable BVD</ButtonText>

         </Strings>

       </Button>

 

@@ -142,7 +143,7 @@
       <IDSymbol name="cmdidRunVerifier" value="0x0101" />

       <IDSymbol name="cmdidStopVerifier" value="0x0102" />

       <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />

-      <IDSymbol name="cmdidShowErrorModel" value="0x0104" />

+      <IDSymbol name="cmdidToggleBVD" value="0x0104" />

     </GuidSymbol>

 

     <!--

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index e078255d..e55a97aa 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -77,7 +77,10 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand runVerifierCommand;

     private OleMenuCommand stopVerifierCommand;

     private OleMenuCommand toggleSnapshotVerificationCommand;

-    private OleMenuCommand showErrorModelCommand;

+    private OleMenuCommand toggleBVDCommand;

+

+    bool BVDDisabled;

+

     public IMenuProxy MenuProxy { get; set; }

 

 

@@ -132,11 +135,11 @@ namespace DafnyLanguage.DafnyMenu
         toggleSnapshotVerificationCommand = new OleMenuCommand(ToggleSnapshotVerificationCallback, toggleSnapshotVerificationCommandID);

         mcs.AddCommand(toggleSnapshotVerificationCommand);

 

-        var showErrorModelCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidShowErrorModel);

-        showErrorModelCommand = new OleMenuCommand(ShowErrorModelCallback, showErrorModelCommandID);

-        showErrorModelCommand.Enabled = true;

-        showErrorModelCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;

-        mcs.AddCommand(showErrorModelCommand);

+        var showErrorModelCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleBVD);

+        toggleBVDCommand = new OleMenuCommand(ToggleBVDCallback, showErrorModelCommandID);

+        toggleBVDCommand.Enabled = true;

+        toggleBVDCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;

+        mcs.AddCommand(toggleBVDCommand);

 

         var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);

         menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);

@@ -179,7 +182,7 @@ namespace DafnyLanguage.DafnyMenu
         return null;

       }

     }

-    

+

     void ToggleSnapshotVerificationCallback(object sender, EventArgs e)

     {

       var atv = ActiveTextView;

@@ -266,17 +269,14 @@ namespace DafnyLanguage.DafnyMenu
       if (MenuProxy != null && atv != null)

       {

         var visible = MenuProxy.ShowErrorModelCommandEnabled(atv);

-        showErrorModelCommand.Visible = visible;

+        toggleBVDCommand.Visible = visible;

       }

     }

 

-    void ShowErrorModelCallback(object sender, EventArgs e)

+    void ToggleBVDCallback(object sender, EventArgs e)

     {

-      var atv = ActiveTextView;

-      if (MenuProxy != null && atv != null)

-      {

-        MenuProxy.ShowErrorModel(atv);

-      }

+      BVDDisabled = !BVDDisabled;

+      toggleBVDCommand.Text = (BVDDisabled ? "Enable" : "Disable") + " BVD";

     }

 

     public void ExecuteAsCompiling(Action action)

@@ -290,21 +290,24 @@ namespace DafnyLanguage.DafnyMenu
       statusBar.Progress(ref cookie, 0, "", 0, 0);

     }

 

-    public void ShowErrorModel(string model, int id)

+    public void ShowErrorModelInBVD(string model, int id)

     {

-      var window = this.FindToolWindow(typeof(BvdToolWindow), 0, true);

-      if ((window == null) || (window.Frame == null))

+      if (!BVDDisabled)

       {

-        throw new NotSupportedException("Can not create BvdToolWindow.");

-      }

+        var window = this.FindToolWindow(typeof(BvdToolWindow), 0, true);

+        if ((window == null) || (window.Frame == null))

+        {

+          throw new NotSupportedException("Can not create BvdToolWindow.");

+        }

 

-      BvdToolWindow.BVD.HideMenuStrip();

-      BvdToolWindow.BVD.HideStateList();

-      BvdToolWindow.BVD.ReadModel(model);

-      BvdToolWindow.BVD.SetState(id, true);

+        BvdToolWindow.BVD.HideMenuStrip();

+        BvdToolWindow.BVD.HideStateList();

+        BvdToolWindow.BVD.ReadModel(model);

+        BvdToolWindow.BVD.SetState(id, true);

 

-      IVsWindowFrame windowFrame = (IVsWindowFrame)window.Frame;

-      Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(windowFrame.Show());

+        IVsWindowFrame windowFrame = (IVsWindowFrame)window.Frame;

+        Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(windowFrame.Show());

+      }

     }

 

     #endregion

diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index f5905ea3..f3452cb9 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -11,6 +11,6 @@ namespace DafnyLanguage.DafnyMenu
     public const uint cmdidStopVerifier = 0x102;

     public const uint cmdidMenu = 0x1021;

     public static uint cmdidToggleSnapshotVerification = 0x103;

-    public const uint cmdidShowErrorModel = 0x104;

+    public const uint cmdidToggleBVD = 0x104;

   };

 }
\ No newline at end of file