DafnyExtension: Added a button to the menu for stopping/starting the verifier.

4 files changed, 78 insertions, 1 deletions

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