summaryrefslogtreecommitdiff
path: root/Source/DafnyMenu
diff options
context:
space:
mode:
Diffstat (limited to 'Source/DafnyMenu')
-rw-r--r--Source/DafnyMenu/DafnyMenu.csproj59
-rw-r--r--Source/DafnyMenu/DafnyMenu.vsct21
-rw-r--r--Source/DafnyMenu/DafnyMenuPackage.cs63
-rw-r--r--Source/DafnyMenu/PkgCmdID.cs2
-rw-r--r--Source/DafnyMenu/packages.config29
-rw-r--r--Source/DafnyMenu/source.extension.vsixmanifest3
6 files changed, 161 insertions, 16 deletions
diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
index 503b3d0c..2a222038 100644
--- a/Source/DafnyMenu/DafnyMenu.csproj
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -62,22 +62,50 @@
</ItemGroup>
<ItemGroup>
<Reference Include="Microsoft.VisualStudio.Shell.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Editor, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.ComponentModelHost, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="Microsoft.VisualStudio.Editor, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Editor.11.0.4\lib\net45\Microsoft.VisualStudio.Editor.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.ComponentModelHost, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.ComponentModelHost.11.0.4\lib\net45\Microsoft.VisualStudio.ComponentModelHost.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Shell.11.11.0.4\lib\net45\Microsoft.VisualStudio.Shell.11.0.dll</HintPath>
+ </Reference>
<Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.OLE.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0, Version=9.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.CoreUtility, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="Microsoft.VisualStudio.OLE.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <HintPath>..\packages\VSSDK.OLE.Interop.7.0.4\lib\net20\Microsoft.VisualStudio.OLE.Interop.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Shell.Interop.11.11.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.11.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Shell.Interop.10.10.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.10.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <HintPath>..\packages\VSSDK.Shell.Interop.8.8.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.8.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0, Version=9.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <HintPath>..\packages\VSSDK.Shell.Interop.9.9.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.9.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.CoreUtility, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.CoreUtility.11.0.4\lib\net45\Microsoft.VisualStudio.CoreUtility.dll</HintPath>
+ </Reference>
<Reference Include="Microsoft.VisualStudio.TextManager.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Text.Data, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Text.UI, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Language.StandardClassification, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="Microsoft.VisualStudio.Text.Data, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.Data.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.Logic.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.UI, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.UI.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.UI.Wpf.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Language.StandardClassification, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Language.11.0.4\lib\net45\Microsoft.VisualStudio.Language.StandardClassification.dll</HintPath>
+ </Reference>
</ItemGroup>
<ItemGroup>
<Reference Include="PresentationCore" />
@@ -127,6 +155,9 @@
</EmbeddedResource>
</ItemGroup>
<ItemGroup>
+ <None Include="packages.config">
+ <SubType>Designer</SubType>
+ </None>
<None Include="source.extension.vsixmanifest">
<SubType>Designer</SubType>
</None>
diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 4c4b1403..02ffcf48 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -112,6 +112,15 @@
</Strings>
</Button>
+ <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleAutomaticInduction" priority="0x0106" type="Button">
+ <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
+ <CommandFlag>DynamicVisibility</CommandFlag>
+ <CommandFlag>TextChanges</CommandFlag>
+ <Strings>
+ <ButtonText>Disable automatic induction</ButtonText>
+ </Strings>
+ </Button>
+
<Button guid="guidDafnyMenuCmdSet" id="cmdidToggleBVD" priority="0x010a" type="Button">
<Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
<CommandFlag>DynamicVisibility</CommandFlag>
@@ -122,6 +131,16 @@
</Strings>
</Button>
+ <Button guid="guidDafnyMenuCmdSet" id="cmdidDiagnoseTimeouts" priority="0x0107" 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 +173,8 @@
<IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />
<IDSymbol name="cmdidToggleBVD" value="0x0104" />
<IDSymbol name="cmdidToggleMoreAdvancedSnapshotVerification" value="0x0105" />
+ <IDSymbol name="cmdidToggleAutomaticInduction" value="0x0106" />
+ <IDSymbol name="cmdidDiagnoseTimeouts" value="0x0107" />
</GuidSymbol>
<!--
diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 0acf3554..0addda47 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -28,6 +28,12 @@ namespace DafnyLanguage.DafnyMenu
bool MoreAdvancedSnapshotVerificationCommandEnabled(IWpfTextView activeTextView);
+ bool ToggleAutomaticInduction(IWpfTextView activeTextView);
+
+
+ bool AutomaticInductionCommandEnabled(IWpfTextView activeTextView);
+
+
bool StopVerifierCommandEnabled(IWpfTextView activeTextView);
@@ -53,6 +59,12 @@ namespace DafnyLanguage.DafnyMenu
void ShowErrorModel(IWpfTextView activeTextView);
+
+
+ bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView);
+
+
+ void DiagnoseTimeouts(IWpfTextView activeTextView);
}
@@ -87,7 +99,9 @@ namespace DafnyLanguage.DafnyMenu
private OleMenuCommand stopVerifierCommand;
private OleMenuCommand toggleSnapshotVerificationCommand;
private OleMenuCommand toggleMoreAdvancedSnapshotVerificationCommand;
+ private OleMenuCommand toggleAutomaticInductionCommand;
private OleMenuCommand toggleBVDCommand;
+ private OleMenuCommand diagnoseTimeoutsCommand;
bool BVDDisabled;
@@ -151,12 +165,24 @@ namespace DafnyLanguage.DafnyMenu
toggleMoreAdvancedSnapshotVerificationCommand.BeforeQueryStatus += toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus;
mcs.AddCommand(toggleMoreAdvancedSnapshotVerificationCommand);
+ var toggleAutomaticInductionCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleAutomaticInduction);
+ toggleAutomaticInductionCommand = new OleMenuCommand(ToggleAutomaticInductionCallback, toggleAutomaticInductionCommandID);
+ toggleAutomaticInductionCommand.Enabled = true;
+ toggleAutomaticInductionCommand.BeforeQueryStatus += toggleAutomaticInductionCommand_BeforeQueryStatus;
+ mcs.AddCommand(toggleAutomaticInductionCommand);
+
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 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;
@@ -221,6 +247,14 @@ namespace DafnyLanguage.DafnyMenu
}
}
+ void ToggleAutomaticInductionCallback(object sender, EventArgs e) {
+ var atv = ActiveTextView;
+ if (MenuProxy != null && atv != null) {
+ var nowAutomatic = MenuProxy.ToggleAutomaticInduction(atv);
+ toggleAutomaticInductionCommand.Text = (nowAutomatic ? "Disable" : "Enable") + " automatic induction";
+ }
+ }
+
void stopVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)
{
var atv = ActiveTextView;
@@ -301,6 +335,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;
@@ -311,12 +355,29 @@ namespace DafnyLanguage.DafnyMenu
}
}
+ private void toggleAutomaticInductionCommand_BeforeQueryStatus(object sender, EventArgs e) {
+ var atv = ActiveTextView;
+ if (MenuProxy != null && atv != null) {
+ var visible = MenuProxy.AutomaticInductionCommandEnabled(atv);
+ toggleAutomaticInductionCommand.Visible = visible;
+ }
+ }
+
void ToggleBVDCallback(object sender, EventArgs e)
{
BVDDisabled = !BVDDisabled;
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));
@@ -347,7 +408,7 @@ namespace DafnyLanguage.DafnyMenu
var window = this.FindToolWindow(typeof(BvdToolWindow), 0, true);
if ((window == null) || (window.Frame == null))
{
- throw new NotSupportedException("Can not create BvdToolWindow.");
+ throw new NotSupportedException("Cannot create BvdToolWindow.");
}
BvdToolWindow.BVD.HideMenuStrip();
diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index b6f30145..ba4b786d 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -13,5 +13,7 @@ namespace DafnyLanguage.DafnyMenu
public static uint cmdidToggleSnapshotVerification = 0x103;
public const uint cmdidToggleBVD = 0x104;
public static uint cmdidToggleMoreAdvancedSnapshotVerification = 0x105;
+ public static uint cmdidToggleAutomaticInduction = 0x106;
+ public static uint cmdidDiagnoseTimeouts = 0x107;
};
} \ No newline at end of file
diff --git a/Source/DafnyMenu/packages.config b/Source/DafnyMenu/packages.config
new file mode 100644
index 00000000..60f856c5
--- /dev/null
+++ b/Source/DafnyMenu/packages.config
@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="utf-8"?>
+<packages>
+ <package id="VSSDK.ComponentModelHost" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.ComponentModelHost.11" version="11.0.3" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.CoreUtility" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.CoreUtility.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.DTE" version="7.0.4" targetFramework="net45" />
+ <package id="VSSDK.Editor" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.IDE" version="7.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.IDE.10" version="10.0.4" targetFramework="net45" />
+ <package id="VSSDK.IDE.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.IDE.8" version="8.0.4" targetFramework="net45" />
+ <package id="VSSDK.IDE.9" version="9.0.4" targetFramework="net45" />
+ <package id="VSSDK.Language" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.Language.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.OLE.Interop" version="7.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.Shell.Immutable.10" version="10.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Immutable.11" version="11.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop" version="7.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop.10" version="10.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop.11" version="11.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop.8" version="8.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop.9" version="9.0.4" targetFramework="net45" />
+ <package id="VSSDK.Text" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.Text.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.TextManager.Interop" version="7.0.4" targetFramework="net45" />
+ <package id="VSSDK.TextManager.Interop.8" version="8.0.4" targetFramework="net45" />
+</packages>
diff --git a/Source/DafnyMenu/source.extension.vsixmanifest b/Source/DafnyMenu/source.extension.vsixmanifest
index 7beeb69e..814374ee 100644
--- a/Source/DafnyMenu/source.extension.vsixmanifest
+++ b/Source/DafnyMenu/source.extension.vsixmanifest
@@ -6,7 +6,8 @@
<Description xml:space="preserve">This is a menu for interacting with Dafny.</Description>
</Metadata>
<Installation InstalledByMsi="false">
- <InstallationTarget Version="[11.0,13.0)" Id="Microsoft.VisualStudio.Pro" />
+ <InstallationTarget Version="[11.0,15.0)" Id="Microsoft.VisualStudio.Pro" />
+ <InstallationTarget Version="[14.0,15.0)" Id="Microsoft.VisualStudio.Community" />
</Installation>
<Dependencies>
<Dependency Id="Microsoft.Framework.NDP" DisplayName="Microsoft .NET Framework" d:Source="Manual" Version="4.5" />
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 16:02:18 +0000