From ef3ccef52b432a7d5c8c7db2add8102bd281b58c Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sun, 26 May 2013 18:44:37 -0700
Subject: DafnyExtension: Added a button to the menu for stopping/starting the
 verifier.

---
 Source/DafnyMenu/DafnyMenu.csproj    |  3 +-
 Source/DafnyMenu/DafnyMenu.vsct      | 20 +++++++++++++
 Source/DafnyMenu/DafnyMenuPackage.cs | 54 ++++++++++++++++++++++++++++++++++++
 Source/DafnyMenu/PkgCmdID.cs         |  2 ++
 4 files changed, 78 insertions(+), 1 deletion(-)

(limited to 'Source/DafnyMenu')

diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
index 3df7f083..e3500e26 100644
--- a/Source/DafnyMenu/DafnyMenu.csproj
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -25,10 +25,11 @@
     <DebugSymbols>true</DebugSymbols>
     <DebugType>full</DebugType>
     <Optimize>false</Optimize>
-    <OutputPath>bin\Debug\</OutputPath>
+    <OutputPath>..\..\Binaries\</OutputPath>
     <DefineConstants>DEBUG;TRACE</DefineConstants>
     <ErrorReport>prompt</ErrorReport>
     <WarningLevel>4</WarningLevel>
+    <CopyVsixExtensionFiles>False</CopyVsixExtensionFiles>
   </PropertyGroup>
   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
     <DebugType>pdbonly</DebugType>
diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 1d0c783b..812a06e8 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -77,6 +77,24 @@
         </Strings>
       </Button>
 
+      <Button guid="guidDafnyMenuCmdSet" id="cmdidRunVerifier" priority="0x0101" type="Button">
+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
+        <CommandFlag>DefaultInvisible</CommandFlag>
+        <CommandFlag>DynamicVisibility</CommandFlag>
+        <Strings>
+          <ButtonText>Run verifier</ButtonText>
+        </Strings>
+      </Button>
+
+      <Button guid="guidDafnyMenuCmdSet" id="cmdidStopVerifier" priority="0x0102" type="Button">
+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
+        <CommandFlag>DefaultInvisible</CommandFlag>
+        <CommandFlag>DynamicVisibility</CommandFlag>
+        <Strings>
+          <ButtonText>Stop verifier</ButtonText>
+        </Strings>
+      </Button>
+
     </Buttons>
 
     <!--The bitmaps section is used to define the bitmaps that are used for the commands.-->
@@ -104,6 +122,8 @@
     <GuidSymbol name="guidDafnyMenuCmdSet" value="{393ad46d-e125-41ce-84ee-b4d552d5ba16}">
       <IDSymbol name="DafnyMenuGroup" value="0x1020" />
       <IDSymbol name="cmdidCompile" value="0x0100" />
+      <IDSymbol name="cmdidRunVerifier" value="0x0101" />
+      <IDSymbol name="cmdidStopVerifier" value="0x0102" />
     </GuidSymbol>
 
     <!--
diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index c0784955..3362f2b3 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -36,6 +36,8 @@ namespace DafnyLanguage.DafnyMenu
 
     private OleMenuCommand compileCommand;
     private OleMenuCommand menuCommand;
+    private OleMenuCommand runVerifierCommand;
+    private OleMenuCommand stopVerifierCommand;
 
     /// <summary>
     /// Default constructor of the package.
@@ -72,6 +74,18 @@ namespace DafnyLanguage.DafnyMenu
         compileCommand.BeforeQueryStatus += compileCommand_BeforeQueryStatus;
         mcs.AddCommand(compileCommand);
 
+        var runVerifierCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidRunVerifier);
+        runVerifierCommand = new OleMenuCommand(RunVerifierCallback, runVerifierCommandID);
+        runVerifierCommand.Enabled = true;
+        runVerifierCommand.BeforeQueryStatus += runVerifierCommand_BeforeQueryStatus;
+        mcs.AddCommand(runVerifierCommand);
+
+        var stopVerifierCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidStopVerifier);
+        stopVerifierCommand = new OleMenuCommand(StopVerifierCallback, stopVerifierCommandID);
+        stopVerifierCommand.Enabled = true;
+        stopVerifierCommand.BeforeQueryStatus += stopVerifierCommand_BeforeQueryStatus;
+        mcs.AddCommand(stopVerifierCommand);
+
         var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);
         menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);
         menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;
@@ -81,6 +95,28 @@ namespace DafnyLanguage.DafnyMenu
       }
     }
 
+    private void StopVerifierCallback(object sender, EventArgs e)
+    {
+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
+      DafnyLanguage.ProgressTagger tagger;
+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);
+      if (tagger != null)
+      {
+        tagger.StopVerification();
+      }
+    }
+
+    private void RunVerifierCallback(object sender, EventArgs e)
+    {
+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
+      DafnyLanguage.ProgressTagger tagger;
+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);
+      if (tagger != null)
+      {
+        tagger.StartVerification();
+      }
+    }
+
     void menuCommand_BeforeQueryStatus(object sender, EventArgs e)
     {
       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
@@ -89,6 +125,24 @@ namespace DafnyLanguage.DafnyMenu
       menuCommand.Enabled = isActive;
     }
 
+    void runVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)
+    {
+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
+      DafnyLanguage.ProgressTagger tagger;
+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);  
+      runVerifierCommand.Visible = tagger != null && tagger.VerificationDisabled;
+      runVerifierCommand.Enabled = tagger != null && tagger.VerificationDisabled;
+    }
+
+    void stopVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)
+    {
+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
+      DafnyLanguage.ProgressTagger tagger;
+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);  
+      stopVerifierCommand.Visible = !(tagger != null && tagger.VerificationDisabled);
+      stopVerifierCommand.Enabled = !(tagger != null && tagger.VerificationDisabled);
+    }
+
     void compileCommand_BeforeQueryStatus(object sender, EventArgs e)
     {
       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index 1b786829..5f0213cc 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -7,6 +7,8 @@ namespace DafnyLanguage.DafnyMenu
   static class PkgCmdIDList
   {
     public const uint cmdidCompile = 0x100;
+    public const uint cmdidRunVerifier = 0x101;
+    public const uint cmdidStopVerifier = 0x102;
     public const uint cmdidMenu = 0x1021;
   };
 }
\ No newline at end of file
-- 
cgit v1.2.3