From 59cfcbb7ac83a23e7df3cb1e85c58167fc07af65 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 23 May 2013 17:55:34 -0700 Subject: DafnyExtension: Added menu for invoking specific Dafny functionality (e.g., compilation). --- Source/DafnyMenu/DafnyMenu.csproj | 181 +++++++++++++++++++++++++ Source/DafnyMenu/DafnyMenu.vsct | 121 +++++++++++++++++ Source/DafnyMenu/DafnyMenuPackage.cs | 126 +++++++++++++++++ Source/DafnyMenu/GlobalSuppressions.cs | 1 + Source/DafnyMenu/Guids.cs | 15 ++ Source/DafnyMenu/PkgCmdID.cs | 12 ++ Source/DafnyMenu/Properties/AssemblyInfo.cs | 36 +++++ Source/DafnyMenu/Resources.Designer.cs | 72 ++++++++++ Source/DafnyMenu/Resources.resx | 129 ++++++++++++++++++ Source/DafnyMenu/Resources/Images.png | Bin 0 -> 989 bytes Source/DafnyMenu/Resources/Package.ico | Bin 0 -> 2998 bytes Source/DafnyMenu/VSPackage.resx | 140 +++++++++++++++++++ Source/DafnyMenu/source.extension.vsixmanifest | 18 +++ 13 files changed, 851 insertions(+) create mode 100644 Source/DafnyMenu/DafnyMenu.csproj create mode 100644 Source/DafnyMenu/DafnyMenu.vsct create mode 100644 Source/DafnyMenu/DafnyMenuPackage.cs create mode 100644 Source/DafnyMenu/GlobalSuppressions.cs create mode 100644 Source/DafnyMenu/Guids.cs create mode 100644 Source/DafnyMenu/PkgCmdID.cs create mode 100644 Source/DafnyMenu/Properties/AssemblyInfo.cs create mode 100644 Source/DafnyMenu/Resources.Designer.cs create mode 100644 Source/DafnyMenu/Resources.resx create mode 100644 Source/DafnyMenu/Resources/Images.png create mode 100644 Source/DafnyMenu/Resources/Package.ico create mode 100644 Source/DafnyMenu/VSPackage.resx create mode 100644 Source/DafnyMenu/source.extension.vsixmanifest (limited to 'Source/DafnyMenu') diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj new file mode 100644 index 00000000..3df7f083 --- /dev/null +++ b/Source/DafnyMenu/DafnyMenu.csproj @@ -0,0 +1,181 @@ + + + + 11.0 + 11.0 + $(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion) + + + + Debug + AnyCPU + 2.0 + {CA0848D3-3E4F-410E-8AC6-D6125A2B8E30} + {82b43b9b-a64c-4715-b499-d71e9ca2bd60};{60dc8134-eba5-43b8-bcc9-bb4bc16c2548};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC} + Library + Properties + DafnyLanguage.DafnyMenu + DafnyMenu + false + + + v4.5 + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + true + + + + ..\..\Binaries\DafnyPipeline.dll + + + + + + + + + true + + + + + + + + + + + + + + + + + {80CC9F66-E7D8-4DDD-85B6-D9E6CD0E93E2} + 8 + 0 + 0 + primary + False + False + + + {26AD1324-4B7C-44BC-84F8-B86AED45729F} + 10 + 0 + 0 + primary + False + False + + + {1A31287A-4D7D-413E-8E32-3B374931BD89} + 8 + 0 + 0 + primary + False + False + + + {2CE2370E-D744-4936-A090-3FFFE667B0E1} + 9 + 0 + 0 + primary + False + False + + + {1CBA492E-7263-47BB-87FE-639000619B15} + 8 + 0 + 0 + primary + False + False + + + {00020430-0000-0000-C000-000000000046} + 2 + 0 + 0 + primary + False + False + + + + + + True + True + Resources.resx + + + + + + + + + ResXFileCodeGenerator + Resources.Designer.cs + Designer + + + true + VSPackage + + + + + Designer + + + + + Menus.ctmenu + + + + + + + + + + + {6e9a5e14-0763-471c-a129-80a879d9e7ba} + DafnyExtension + + + + true + + + + + \ No newline at end of file diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct new file mode 100644 index 00000000..1d0c783b --- /dev/null +++ b/Source/DafnyMenu/DafnyMenu.vsct @@ -0,0 +1,121 @@ + + + + + + + + + + + + + + + + + + + + + + + DefaultInvisible + DynamicVisibility + + + Dafny + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs new file mode 100644 index 00000000..c0784955 --- /dev/null +++ b/Source/DafnyMenu/DafnyMenuPackage.cs @@ -0,0 +1,126 @@ +using System; +using System.Diagnostics; +using System.Globalization; +using System.Runtime.InteropServices; +using System.ComponentModel.Design; +using Microsoft.Win32; +using Microsoft.VisualStudio; +using Microsoft.VisualStudio.Shell.Interop; +using Microsoft.VisualStudio.OLE.Interop; +using Microsoft.VisualStudio.Shell; + +namespace DafnyLanguage.DafnyMenu +{ + /// + /// This is the class that implements the package exposed by this assembly. + /// + /// The minimum requirement for a class to be considered a valid package for Visual Studio + /// is to implement the IVsPackage interface and register itself with the shell. + /// This package uses the helper classes defined inside the Managed Package Framework (MPF) + /// to do it: it derives from the Package class that provides the implementation of the + /// IVsPackage interface and uses the registration attributes defined in the framework to + /// register itself and its components with the shell. + /// + // This attribute tells the PkgDef creation utility (CreatePkgDef.exe) that this class is + // a package. + [PackageRegistration(UseManagedResourcesOnly = true)] + // This attribute is used to register the information needed to show this package + // in the Help/About dialog of Visual Studio. + [InstalledProductRegistration("#110", "#112", "1.0", IconResourceID = 400)] + // This attribute is needed to let the shell know that this package exposes some menus. + [ProvideMenuResource("Menus.ctmenu", 1)] + [ProvideAutoLoad("{6c7ed99a-206a-4937-9e08-b389de175f68}")] + [Guid(GuidList.guidDafnyMenuPkgString)] + public sealed class DafnyMenuPackage : Package + { + + private OleMenuCommand compileCommand; + private OleMenuCommand menuCommand; + + /// + /// Default constructor of the package. + /// Inside this method you can place any initialization code that does not require + /// any Visual Studio service because at this point the package object is created but + /// not sited yet inside Visual Studio environment. The place to do all the other + /// initialization is the Initialize method. + /// + public DafnyMenuPackage() + { + Debug.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString())); + } + + + #region Package Members + + /// + /// Initialization of the package; this method is called right after the package is sited, so this is the place + /// where you can put all the initialization code that rely on services provided by VisualStudio. + /// + protected override void Initialize() + { + Debug.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering Initialize() of: {0}", this.ToString())); + base.Initialize(); + + // Add our command handlers for menu (commands must exist in the .vsct file) + var mcs = GetService(typeof(IMenuCommandService)) as OleMenuCommandService; + if (null != mcs) + { + // Create the command for the menu item. + var compileCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidCompile); + compileCommand = new OleMenuCommand(CompileCallback, compileCommandID); + compileCommand.Enabled = false; + compileCommand.BeforeQueryStatus += compileCommand_BeforeQueryStatus; + mcs.AddCommand(compileCommand); + + var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu); + menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID); + menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus; + menuCommand.Enabled = true; + var s = menuCommand.OleStatus; + mcs.AddCommand(menuCommand); + } + } + + void menuCommand_BeforeQueryStatus(object sender, EventArgs e) + { + var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE; + var isActive = dte.ActiveDocument.FullName.EndsWith(".dfy"); + menuCommand.Visible = isActive; + menuCommand.Enabled = isActive; + } + + void compileCommand_BeforeQueryStatus(object sender, EventArgs e) + { + var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE; + Microsoft.Dafny.Program program; + DafnyLanguage.ResolverTagger.Programs.TryGetValue(dte.ActiveDocument.FullName, out program); + compileCommand.Enabled = (program != null); + } + + #endregion + + + /// + /// This function is the callback used to execute a command when the a menu item is clicked. + /// See the Initialize method to see how the menu item is associated to this function using + /// the OleMenuCommandService service and the MenuCommand class. + /// + private void CompileCallback(object sender, EventArgs e) + { + var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE; + Microsoft.Dafny.Program program; + DafnyLanguage.ResolverTagger.Programs.TryGetValue(dte.ActiveDocument.FullName, out program); + + if (program != null) + { + IVsStatusbar statusBar = (IVsStatusbar)GetGlobalService(typeof(SVsStatusbar)); + uint cookie = 0; + statusBar.Progress(ref cookie, 1, "Compiling...", 0, 0); + + DafnyDriver.Compile(program); + + statusBar.Progress(ref cookie, 0, "", 0, 0); + } + } + } +} diff --git a/Source/DafnyMenu/GlobalSuppressions.cs b/Source/DafnyMenu/GlobalSuppressions.cs new file mode 100644 index 00000000..3689ed23 --- /dev/null +++ b/Source/DafnyMenu/GlobalSuppressions.cs @@ -0,0 +1 @@ +[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1017:MarkAssembliesWithComVisible")] diff --git a/Source/DafnyMenu/Guids.cs b/Source/DafnyMenu/Guids.cs new file mode 100644 index 00000000..dc392c09 --- /dev/null +++ b/Source/DafnyMenu/Guids.cs @@ -0,0 +1,15 @@ +// Guids.cs +// MUST match guids.h +using System; + +namespace DafnyLanguage.DafnyMenu +{ + static class GuidList + { + public const string guidDafnyMenuPkgString = "e1baf989-88a6-4acf-8d97-e0dc243476aa"; + public const string guidDafnyMenuCmdSetString = "393ad46d-e125-41ce-84ee-b4d552d5ba16"; + + public static readonly Guid guidDafnyMenuCmdSet = new Guid(guidDafnyMenuCmdSetString); + public static readonly Guid guidDafnyMenuPkgSet = new Guid(guidDafnyMenuPkgString); + }; +} \ No newline at end of file diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs new file mode 100644 index 00000000..1b786829 --- /dev/null +++ b/Source/DafnyMenu/PkgCmdID.cs @@ -0,0 +1,12 @@ +// PkgCmdID.cs +// MUST match PkgCmdID.h +using System; + +namespace DafnyLanguage.DafnyMenu +{ + static class PkgCmdIDList + { + public const uint cmdidCompile = 0x100; + public const uint cmdidMenu = 0x1021; + }; +} \ No newline at end of file diff --git a/Source/DafnyMenu/Properties/AssemblyInfo.cs b/Source/DafnyMenu/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..91380a74 --- /dev/null +++ b/Source/DafnyMenu/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System; +using System.Reflection; +using System.Resources; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("DafnyMenu")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("Microsoft Research")] +[assembly: AssemblyProduct("DafnyMenu")] +[assembly: AssemblyCopyright("")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] +[assembly: ComVisible(false)] +[assembly: CLSCompliant(false)] +[assembly: NeutralResourcesLanguage("en-US")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Revision and Build Numbers +// by using the '*' as shown below: + +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] + + + diff --git a/Source/DafnyMenu/Resources.Designer.cs b/Source/DafnyMenu/Resources.Designer.cs new file mode 100644 index 00000000..f9fefb73 --- /dev/null +++ b/Source/DafnyMenu/Resources.Designer.cs @@ -0,0 +1,72 @@ +//------------------------------------------------------------------------------ +// +// This code was generated by a tool. +// Runtime Version:4.0.30319.18033 +// +// Changes to this file may cause incorrect behavior and will be lost if +// the code is regenerated. +// +//------------------------------------------------------------------------------ + +namespace DafnyLanguage.DafnyMenu +{ + using System; + + + /// + /// A strongly-typed resource class, for looking up localized strings, etc. + /// + // This class was auto-generated by the StronglyTypedResourceBuilder + // class via a tool like ResGen or Visual Studio. + // To add or remove a member, edit your .ResX file then rerun ResGen + // with the /str option, or rebuild your VS project. + [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")] + [global::System.Diagnostics.DebuggerNonUserCodeAttribute()] + [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()] + internal class Resources + { + + private static global::System.Resources.ResourceManager resourceMan; + + private static global::System.Globalization.CultureInfo resourceCulture; + + [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")] + internal Resources() + { + } + + /// + /// Returns the cached ResourceManager instance used by this class. + /// + [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] + internal static global::System.Resources.ResourceManager ResourceManager + { + get + { + if (object.ReferenceEquals(resourceMan, null)) + { + global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("DafnyLanguage.DafnyMenu.Resources", typeof(Resources).Assembly); + resourceMan = temp; + } + return resourceMan; + } + } + + /// + /// Overrides the current thread's CurrentUICulture property for all + /// resource lookups using this strongly typed resource class. + /// + [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] + internal static global::System.Globalization.CultureInfo Culture + { + get + { + return resourceCulture; + } + set + { + resourceCulture = value; + } + } + } +} diff --git a/Source/DafnyMenu/Resources.resx b/Source/DafnyMenu/Resources.resx new file mode 100644 index 00000000..352987aa --- /dev/null +++ b/Source/DafnyMenu/Resources.resx @@ -0,0 +1,129 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + text/microsoft-resx + + + 2.0 + + + System.Resources.ResXResourceReader, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 + + + System.Resources.ResXResourceWriter, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 + + \ No newline at end of file diff --git a/Source/DafnyMenu/Resources/Images.png b/Source/DafnyMenu/Resources/Images.png new file mode 100644 index 00000000..51fe0d15 Binary files /dev/null and b/Source/DafnyMenu/Resources/Images.png differ diff --git a/Source/DafnyMenu/Resources/Package.ico b/Source/DafnyMenu/Resources/Package.ico new file mode 100644 index 00000000..449296f4 Binary files /dev/null and b/Source/DafnyMenu/Resources/Package.ico differ diff --git a/Source/DafnyMenu/VSPackage.resx b/Source/DafnyMenu/VSPackage.resx new file mode 100644 index 00000000..8ab9cc50 --- /dev/null +++ b/Source/DafnyMenu/VSPackage.resx @@ -0,0 +1,140 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + text/microsoft-resx + + + 2.0 + + + System.Resources.ResXResourceReader, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 + + + System.Resources.ResXResourceWriter, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 + + + + DafnyMenu + + + This is a menu for invoking Dafny. + + + Resources\Package.ico;System.Drawing.Icon, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a + + \ No newline at end of file diff --git a/Source/DafnyMenu/source.extension.vsixmanifest b/Source/DafnyMenu/source.extension.vsixmanifest new file mode 100644 index 00000000..08ea6bef --- /dev/null +++ b/Source/DafnyMenu/source.extension.vsixmanifest @@ -0,0 +1,18 @@ + + + + + DafnyMenu + This is a menu for interacting with Dafny. + + + + + + + + + + + + -- cgit v1.2.3