Merge

6 files changed, 194 insertions, 130 deletions

diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
index 7fb6cfab..c3a1647b 100644
--- a/Source/DafnyMenu/DafnyMenu.csproj
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003" ToolsVersion="4.0">

   <PropertyGroup>

     <MinimumVisualStudioVersion>11.0</MinimumVisualStudioVersion>

@@ -30,14 +30,14 @@
     <DefineConstants>DEBUG;TRACE</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

-    <CopyVsixExtensionFiles>False</CopyVsixExtensionFiles>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

     <Prefer32Bit>false</Prefer32Bit>

+    <DeployExtension>False</DeployExtension>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

     <DebugType>pdbonly</DebugType>

     <Optimize>true</Optimize>

-    <OutputPath>bin\Release\</OutputPath>

+    <OutputPath>..\..\Binaries\</OutputPath>

     <DefineConstants>TRACE</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

@@ -48,20 +48,33 @@
     <Reference Include="DafnyPipeline">

       <HintPath>..\..\Binaries\DafnyPipeline.dll</HintPath>

     </Reference>

+    <Reference Include="Model">

+      <HintPath>..\..\..\boogie\Binaries\Model.dll</HintPath>

+    </Reference>

+    <Reference Include="ModelViewer">

+      <HintPath>..\..\..\boogie\Binaries\ModelViewer.dll</HintPath>

+    </Reference>

+  </ItemGroup>

+  <ItemGroup>

+    <Reference Include="Microsoft.VisualStudio.CoreUtility" />

+    <Reference Include="Microsoft.VisualStudio.ComponentModelHost" />

+    <Reference Include="Microsoft.VisualStudio.Editor" />

     <Reference Include="Microsoft.VisualStudio.OLE.Interop" />

-    <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

-    <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

+    <Reference Include="Microsoft.VisualStudio.Shell.11.0" />

+    <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0" />

     <Reference Include="Microsoft.VisualStudio.Shell.Interop" />

-    <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+    <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0">

       <EmbedInteropTypes>True</EmbedInteropTypes>

     </Reference>

-    <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />

+    <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0" />

     <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0" />

     <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0" />

-    <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

-    <Reference Include="ModelViewer">

-      <HintPath>..\..\..\boogie\Binaries\ModelViewer.dll</HintPath>

-    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Text.Logic" />

+    <Reference Include="Microsoft.VisualStudio.Text.UI" />

+    <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf" />

+    <Reference Include="Microsoft.VisualStudio.TextManager.Interop" />

+  </ItemGroup>

+  <ItemGroup>

     <Reference Include="PresentationCore" />

     <Reference Include="PresentationFramework" />

     <Reference Include="System" />

@@ -118,12 +131,6 @@
     </VSCTCompile>

   </ItemGroup>

   <ItemGroup>

-    <ProjectReference Include="..\DafnyExtension\DafnyExtension.csproj">

-      <Project>{6e9a5e14-0763-471c-a129-80a879d9e7ba}</Project>

-      <Name>DafnyExtension</Name>

-    </ProjectReference>

-  </ItemGroup>

-  <ItemGroup>

     <Folder Include="Resources\" />

   </ItemGroup>

   <PropertyGroup>

@@ -131,11 +138,11 @@
   </PropertyGroup>

   <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />

   <Import Project="$(VSToolsPath)\VSSDK\Microsoft.VsSDK.targets" Condition="'$(VSToolsPath)' != ''" />

-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it.

        Other similar extension points exist, see Microsoft.Common.targets.

   <Target Name="BeforeBuild">

   </Target>

   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>
\ No newline at end of file
+</Project>

diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index d23ebc7f..0e8c7855 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -103,12 +103,13 @@
         </Strings>

       </Button>

 

-      <Button guid="guidDafnyMenuCmdSet" id="cmdidShowErrorModel" priority="0x010a" type="Button">

+      <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleBVD" priority="0x010a" type="Button">

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

         <CommandFlag>DynamicVisibility</CommandFlag>

         <CommandFlag>DefaultInvisible</CommandFlag>

+        <CommandFlag>TextChanges</CommandFlag>

         <Strings>

-          <ButtonText>Show model for selected error in BVD</ButtonText>

+          <ButtonText>Disable BVD</ButtonText>

         </Strings>

       </Button>

 

@@ -142,7 +143,7 @@
       <IDSymbol name="cmdidRunVerifier" value="0x0101" />

       <IDSymbol name="cmdidStopVerifier" value="0x0102" />

       <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />

-      <IDSymbol name="cmdidShowErrorModel" value="0x0104" />

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

     </GuidSymbol>

 

     <!--

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 5481141c..e55a97aa 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -2,14 +2,51 @@
 using System.ComponentModel.Design;

 using System.Diagnostics;

 using System.Globalization;

-using System.Linq;

 using System.Runtime.InteropServices;

+using Microsoft.VisualStudio.ComponentModelHost;

+using Microsoft.VisualStudio.Editor;

 using Microsoft.VisualStudio.Shell;

 using Microsoft.VisualStudio.Shell.Interop;

+using Microsoft.VisualStudio.Text.Editor;

+using Microsoft.VisualStudio.TextManager.Interop;

 

 

 namespace DafnyLanguage.DafnyMenu

 {

+

+  public interface IMenuProxy

+  {

+    bool ToggleSnapshotVerification(IWpfTextView activeTextView);

+

+

+    bool StopVerifierCommandEnabled(IWpfTextView activeTextView);

+

+

+    void StopVerifier(IWpfTextView activeTextView);

+

+

+    bool RunVerifierCommandEnabled(IWpfTextView activeTextView);

+

+

+    void RunVerifier(IWpfTextView activeTextView);

+

+

+    bool MenuEnabled(IWpfTextView activeTextView);

+

+

+    bool CompileCommandEnabled(IWpfTextView activeTextView);

+

+

+    void Compile(IWpfTextView activeTextView);

+

+

+    bool ShowErrorModelCommandEnabled(IWpfTextView activeTextView);

+

+

+    void ShowErrorModel(IWpfTextView activeTextView);

+  }

+

+

   /// <summary>

   /// This is the class that implements the package exposed by this assembly.

   ///

@@ -25,7 +62,7 @@ namespace DafnyLanguage.DafnyMenu
   [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")]

+  // [InstalledProductRegistration("#110", "#112", "1.0")]

   // 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}")]

@@ -40,7 +77,12 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand runVerifierCommand;

     private OleMenuCommand stopVerifierCommand;

     private OleMenuCommand toggleSnapshotVerificationCommand;

-    private OleMenuCommand showErrorModelCommand;

+    private OleMenuCommand toggleBVDCommand;

+

+    bool BVDDisabled;

+

+    public IMenuProxy MenuProxy { get; set; }

+

 

     /// <summary>

     /// Default constructor of the package.

@@ -90,15 +132,14 @@ namespace DafnyLanguage.DafnyMenu
         mcs.AddCommand(stopVerifierCommand);

 

         var toggleSnapshotVerificationCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleSnapshotVerification);

-        DafnyDriver.ToggleIncrementalVerification();

         toggleSnapshotVerificationCommand = new OleMenuCommand(ToggleSnapshotVerificationCallback, toggleSnapshotVerificationCommandID);

         mcs.AddCommand(toggleSnapshotVerificationCommand);

 

-        var showErrorModelCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidShowErrorModel);

-        showErrorModelCommand = new OleMenuCommand(ShowErrorModelCallback, showErrorModelCommandID);

-        showErrorModelCommand.Enabled = true;

-        showErrorModelCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;

-        mcs.AddCommand(showErrorModelCommand);

+        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 menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);

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

@@ -108,125 +149,150 @@ namespace DafnyLanguage.DafnyMenu
       }

     }

 

-    private void ToggleSnapshotVerificationCallback(object sender, EventArgs e)

+    internal IVsEditorAdaptersFactoryService editorAdapterFactoryService = null;

+

+    private IWpfTextView ActiveTextView

     {

-      var on = DafnyDriver.ToggleIncrementalVerification();

-      toggleSnapshotVerificationCommand.Text = (on ? "Disable" : "Enable") + " on-demand re-verification";

+      get

+      {

+        var textManager = (IVsTextManager)GetService(typeof(SVsTextManager));

+        if (textManager != null)

+        {

+          IVsTextView view;

+          if (textManager.GetActiveView(1, null, out view) == Microsoft.VisualStudio.VSConstants.S_OK)

+          {

+            if (editorAdapterFactoryService == null)

+            {

+              var componentModel = (IComponentModel)GetService(typeof(SComponentModel));

+              if (componentModel != null)

+              {

+                editorAdapterFactoryService = componentModel.GetService<IVsEditorAdaptersFactoryService>();

+              }

+            }

+            if (editorAdapterFactoryService != null)

+            {

+              var textView = editorAdapterFactoryService.GetWpfTextView(view);

+              if (textView != null)

+              {

+                return textView;

+              }

+            }

+          }

+        }

+        return null;

+      }

     }

 

-    private void StopVerifierCallback(object sender, EventArgs e)

+    void ToggleSnapshotVerificationCallback(object sender, EventArgs e)

     {

-      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      DafnyLanguage.ProgressTagger tagger;

-      if (dte.ActiveDocument != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger))

+      var atv = ActiveTextView;

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

       {

-        tagger.StopVerification();

+        var on = MenuProxy.ToggleSnapshotVerification(atv);

+        toggleSnapshotVerificationCommand.Text = (on ? "Disable" : "Enable") + " on-demand re-verification";

       }

     }

 

-    private void RunVerifierCallback(object sender, EventArgs e)

+    void stopVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

-      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      DafnyLanguage.ProgressTagger tagger;

-      if (dte.ActiveDocument != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger))

+      var atv = ActiveTextView;

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

       {

-        tagger.StartVerification();

+        var disabled = MenuProxy.StopVerifierCommandEnabled(atv);

+        stopVerifierCommand.Visible = !disabled;

+        stopVerifierCommand.Enabled = !disabled;

       }

     }

 

-    void menuCommand_BeforeQueryStatus(object sender, EventArgs e)

+    void StopVerifierCallback(object sender, EventArgs e)

     {

-      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      var isActive = dte.ActiveDocument != null

-                     && dte.ActiveDocument.FullName.EndsWith(".dfy", StringComparison.OrdinalIgnoreCase);

-      menuCommand.Visible = isActive;

-      menuCommand.Enabled = isActive;

+      var atv = ActiveTextView;

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

+      {

+        MenuProxy.StopVerifier(atv);

+      }

     }

 

     void runVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

-      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      DafnyLanguage.ProgressTagger tagger;

-      var enabled = dte.ActiveDocument != null

-                 && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger)

-                 && tagger != null && tagger.VerificationDisabled;

-      runVerifierCommand.Visible = enabled;

-      runVerifierCommand.Enabled = enabled;

+      var atv = ActiveTextView;

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

+      {

+        var enabled = MenuProxy.RunVerifierCommandEnabled(atv);

+        runVerifierCommand.Visible = enabled;

+        runVerifierCommand.Enabled = enabled;

+      }

+    }

+

+    void RunVerifierCallback(object sender, EventArgs e)

+    {

+      var atv = ActiveTextView;

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

+      {

+        MenuProxy.RunVerifier(atv);

+      }

     }

 

-    void stopVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)

+    void menuCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

-      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      DafnyLanguage.ProgressTagger tagger;

-      var disabled = dte.ActiveDocument != null

-                    && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger)

-                    && tagger != null && tagger.VerificationDisabled;

-      stopVerifierCommand.Visible = !disabled;

-      stopVerifierCommand.Enabled = !disabled;

+      var atv = ActiveTextView;

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

+      {

+        var isActive = MenuProxy.MenuEnabled(atv);

+        menuCommand.Visible = isActive;

+        menuCommand.Enabled = isActive;

+      }

     }

 

     void compileCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

-      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      ResolverTagger resolver;

-      var enabled = dte.ActiveDocument != null

-                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)

-                    && resolver.Program != null;

-      compileCommand.Enabled = enabled;

+      var atv = ActiveTextView;

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

+      {

+        var enabled = MenuProxy.CompileCommandEnabled(atv);

+        compileCommand.Enabled = enabled;

+      }

     }

 

-    #endregion

-

-

-    /// <summary>

-    /// 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.

-    /// </summary>

-    private void CompileCallback(object sender, EventArgs e)

+    void CompileCallback(object sender, EventArgs e)

     {

-      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      ResolverTagger resolver;

-

-      if (dte.ActiveDocument != null

-          && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)

-          && resolver.Program != null)

+      var atv = ActiveTextView;

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

       {

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

-        uint cookie = 0;

-        statusBar.Progress(ref cookie, 1, "Compiling...", 0, 0);

-

-        DafnyDriver.Compile(resolver.Program);

-

-        statusBar.Progress(ref cookie, 0, "", 0, 0);

+        MenuProxy.Compile(atv);

       }

     }

 

-    /// <summary>

-    /// Show error model.

-    /// </summary>

-    /// <param name="sender"></param>

-    /// <param name="e"></param>

     void showErrorModelCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

-      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      ResolverTagger resolver;

-      var visible = dte.ActiveDocument != null

-                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)

-                    && resolver.Program != null

-                    && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));

-      showErrorModelCommand.Visible = visible;

+      var atv = ActiveTextView;

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

+      {

+        var visible = MenuProxy.ShowErrorModelCommandEnabled(atv);

+        toggleBVDCommand.Visible = visible;

+      }

+    }

+

+    void ToggleBVDCallback(object sender, EventArgs e)

+    {

+      BVDDisabled = !BVDDisabled;

+      toggleBVDCommand.Text = (BVDDisabled ? "Enable" : "Disable") + " BVD";

     }

 

-    private void ShowErrorModelCallback(object sender, EventArgs e)

+    public void ExecuteAsCompiling(Action action)

     {

-      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

-      ResolverTagger resolver = null;

-      var show = dte.ActiveDocument != null

-                 && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)

-                 && resolver.Program != null

-                 && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));

-      if (show)

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

+      uint cookie = 0;

+      statusBar.Progress(ref cookie, 1, "Compiling...", 0, 0);

+

+      action();

+

+      statusBar.Progress(ref cookie, 0, "", 0, 0);

+    }

+

+    public void ShowErrorModelInBVD(string model, int id)

+    {

+      if (!BVDDisabled)

       {

         var window = this.FindToolWindow(typeof(BvdToolWindow), 0, true);

         if ((window == null) || (window.Frame == null))

@@ -234,16 +300,16 @@ namespace DafnyLanguage.DafnyMenu
           throw new NotSupportedException("Can not create BvdToolWindow.");

         }

 

-        var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));

-        if (selectedError != null)

-        {

-          BvdToolWindow.BVD.ReadModel(selectedError.Model);

-          BvdToolWindow.BVD.SetState(selectedError.SelectedStateId, true);

-        }

+        BvdToolWindow.BVD.HideMenuStrip();

+        BvdToolWindow.BVD.HideStateList();

+        BvdToolWindow.BVD.ReadModel(model);

+        BvdToolWindow.BVD.SetState(id, true);

 

         IVsWindowFrame windowFrame = (IVsWindowFrame)window.Frame;

         Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(windowFrame.Show());

       }

     }

+

+    #endregion

   }

 }

diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index f5905ea3..f3452cb9 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -11,6 +11,6 @@ namespace DafnyLanguage.DafnyMenu
     public const uint cmdidStopVerifier = 0x102;

     public const uint cmdidMenu = 0x1021;

     public static uint cmdidToggleSnapshotVerification = 0x103;

-    public const uint cmdidShowErrorModel = 0x104;

+    public const uint cmdidToggleBVD = 0x104;

   };

 }
\ No newline at end of file
diff --git a/Source/DafnyMenu/Properties/AssemblyInfo.cs b/Source/DafnyMenu/Properties/AssemblyInfo.cs
index 91380a74..b1a5687d 100644
--- a/Source/DafnyMenu/Properties/AssemblyInfo.cs
+++ b/Source/DafnyMenu/Properties/AssemblyInfo.cs
@@ -1,7 +1,6 @@
 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 

@@ -31,6 +30,3 @@ using System.Runtime.InteropServices;
 

 [assembly: AssemblyVersion("1.0.0.0")]

 [assembly: AssemblyFileVersion("1.0.0.0")]

-

-

-

diff --git a/Source/DafnyMenu/VSPackage.resx b/Source/DafnyMenu/VSPackage.resx
index effe10d4..29dcb1b3 100644
--- a/Source/DafnyMenu/VSPackage.resx
+++ b/Source/DafnyMenu/VSPackage.resx
@@ -117,10 +117,4 @@
   <resheader name="writer">

     <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

   </resheader>

-  <data name="110" xml:space="preserve">

-    <value>DafnyMenu</value>

-  </data>

-  <data name="112" xml:space="preserve">

-    <value>This is a menu for invoking Dafny.</value>

-  </data>

 </root>
\ No newline at end of file