From b9ce2ee218e4facd887034422192855aa556eec6 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sun, 28 Jul 2013 17:59:48 -0700
Subject: DafnyExtension: Make it possible to enable and disable BVD.

---
 Source/DafnyMenu/DafnyMenu.vsct      |  7 +++--
 Source/DafnyMenu/DafnyMenuPackage.cs | 53 +++++++++++++++++++-----------------
 Source/DafnyMenu/PkgCmdID.cs         |  2 +-
 3 files changed, 33 insertions(+), 29 deletions(-)

(limited to 'Source/DafnyMenu')

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
-- 
cgit v1.2.3