DafnyExtension: Added experimental support for diagnosing timeouts.

3 files changed, 44 insertions, 0 deletions

diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 4c4b1403..4c9a4913 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -122,6 +122,16 @@
         </Strings>

       </Button>

 

+      <Button guid="guidDafnyMenuCmdSet" id="cmdidDiagnoseTimeouts" priority="0x0106" type="Button">

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

+        <CommandFlag>DynamicVisibility</CommandFlag>

+        <CommandFlag>DefaultInvisible</CommandFlag>

+        <CommandFlag>TextChanges</CommandFlag>

+        <Strings>

+          <ButtonText>Re-verify to diagnose timeouts</ButtonText>

+        </Strings>

+      </Button>

+

     </Buttons>

 

     <!--The bitmaps section is used to define the bitmaps that are used for the commands.-->

@@ -154,6 +164,7 @@
       <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />

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

       <IDSymbol name="cmdidToggleMoreAdvancedSnapshotVerification" value="0x0105" />

+      <IDSymbol name="cmdidDiagnoseTimeouts" value="0x0106" />

     </GuidSymbol>

 

     <!--

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 0acf3554..58c8f0ab 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -53,6 +53,12 @@ namespace DafnyLanguage.DafnyMenu
 

 

     void ShowErrorModel(IWpfTextView activeTextView);

+

+

+    bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView);

+

+

+    void DiagnoseTimeouts(IWpfTextView activeTextView);

   }

 

 

@@ -88,6 +94,7 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand toggleSnapshotVerificationCommand;

     private OleMenuCommand toggleMoreAdvancedSnapshotVerificationCommand;

     private OleMenuCommand toggleBVDCommand;

+    private OleMenuCommand diagnoseTimeoutsCommand;

 

     bool BVDDisabled;

 

@@ -157,6 +164,12 @@ namespace DafnyLanguage.DafnyMenu
         toggleBVDCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;

         mcs.AddCommand(toggleBVDCommand);

 

+        var diagnoseTimeoutsCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidDiagnoseTimeouts);

+        diagnoseTimeoutsCommand = new OleMenuCommand(DiagnoseTimeoutsCallback, diagnoseTimeoutsCommandID);

+        diagnoseTimeoutsCommand.Enabled = true;

+        diagnoseTimeoutsCommand.BeforeQueryStatus += diagnoseTimeoutsCommand_BeforeQueryStatus;

+        mcs.AddCommand(diagnoseTimeoutsCommand);

+

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

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

         menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;

@@ -301,6 +314,16 @@ namespace DafnyLanguage.DafnyMenu
       }

     }

 

+    void diagnoseTimeoutsCommand_BeforeQueryStatus(object sender, EventArgs e)

+    {

+      var atv = ActiveTextView;

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

+      {

+        var visible = MenuProxy.DiagnoseTimeoutsCommandEnabled(atv);

+        diagnoseTimeoutsCommand.Visible = visible;

+      }

+    }

+

     private void toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

       var atv = ActiveTextView;

@@ -317,6 +340,15 @@ namespace DafnyLanguage.DafnyMenu
       toggleBVDCommand.Text = (BVDDisabled ? "Enable" : "Disable") + " BVD";

     }

 

+    void DiagnoseTimeoutsCallback(object sender, EventArgs e)

+    {

+      var atv = ActiveTextView;

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

+      {

+        MenuProxy.DiagnoseTimeouts(atv);

+      }

+    }

+

     public void ExecuteAsCompiling(Action action, TextWriter outputWriter)

     {

       IVsStatusbar statusBar = (IVsStatusbar)GetGlobalService(typeof(SVsStatusbar));

diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index b6f30145..427dd888 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -13,5 +13,6 @@ namespace DafnyLanguage.DafnyMenu
     public static uint cmdidToggleSnapshotVerification = 0x103;

     public const uint cmdidToggleBVD = 0x104;

     public static uint cmdidToggleMoreAdvancedSnapshotVerification = 0x105;

+    public static uint cmdidDiagnoseTimeouts = 0x106;

   };

 }
\ No newline at end of file