DafnyExtension: Did some refactoring to integrate the Dafny menu more tightly.

11 files changed, 308 insertions, 130 deletions

diff --git a/Source/DafnyExtension/ClassificationTagger.cs b/Source/DafnyExtension/ClassificationTagger.cs
index 5be982ed..08157f9c 100644
--- a/Source/DafnyExtension/ClassificationTagger.cs
+++ b/Source/DafnyExtension/ClassificationTagger.cs
@@ -43,7 +43,7 @@ namespace DafnyLanguage
     ITagAggregator<DafnyTokenTag> _aggregator;

     IDictionary<DafnyTokenKind, IClassificationType> _typeMap;

 

-    static bool DafnyMenuWasInitialized;

+    internal static DafnyMenu.DafnyMenuPackage DafnyMenuPackage;

 

     internal DafnyClassifier(ITextBuffer buffer,

                              ITagAggregator<DafnyTokenTag> tagAggregator,

@@ -62,7 +62,7 @@ namespace DafnyLanguage
       _typeMap[DafnyTokenKind.AdditionalInformation] = standards.Other;

       _typeMap[DafnyTokenKind.VariableIdentifierDefinition] = typeService.GetClassificationType("Dafny identifier");

 

-      if (!DafnyMenuWasInitialized)

+      if (DafnyMenuPackage == null)

       {

         // Initialize the Dafny menu.

         var shell = Microsoft.VisualStudio.Shell.Package.GetGlobalService(typeof(Microsoft.VisualStudio.Shell.Interop.SVsShell)) as Microsoft.VisualStudio.Shell.Interop.IVsShell;

@@ -70,9 +70,12 @@ namespace DafnyLanguage
         {

           Microsoft.VisualStudio.Shell.Interop.IVsPackage package = null;

           Guid PackageToBeLoadedGuid = new Guid("e1baf989-88a6-4acf-8d97-e0dc243476aa");

-          shell.LoadPackage(ref PackageToBeLoadedGuid, out package);

+          if (shell.LoadPackage(ref PackageToBeLoadedGuid, out package) == Microsoft.VisualStudio.VSConstants.S_OK)

+          {

+            DafnyMenuPackage = (DafnyMenu.DafnyMenuPackage)package;

+            DafnyMenuPackage.MenuProxy = new MenuProxy(DafnyMenuPackage);

+          }

         }

-        DafnyMenuWasInitialized = true;

       }

     }

 

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index b4f44df0..168e69b5 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -45,6 +45,7 @@ namespace DafnyLanguage
 

         ExecutionEngine.printer = new DummyPrinter();

         ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();

+        ToggleIncrementalVerification();

       }

     }

 

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 4a2a336a..31e344a1 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -1,5 +1,5 @@
-<?xml version="1.0" encoding="utf-8"?>

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

+<?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>

     <VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">11.0</VisualStudioVersion>

@@ -145,6 +145,7 @@
     <Compile Include="GlobalSuppressions.cs" />

     <Compile Include="HoverText.cs" />

     <Compile Include="IdentifierTagger.cs" />

+    <Compile Include="MenuProxy.cs" />

     <Compile Include="ProgressMargin.cs" />

     <Compile Include="OutliningTagger.cs" />

     <Compile Include="ResolverTagger.cs" />

@@ -173,10 +174,18 @@
       <SubType>Designer</SubType>

     </None>

   </ItemGroup>

+  <ItemGroup>

+    <ProjectReference Include="..\DafnyMenu\DafnyMenu.csproj">

+      <Project>{ca0848d3-3e4f-410e-8ac6-d6125a2b8e30}</Project>

+      <Name>DafnyMenu</Name>

+      <IncludeOutputGroupsInVSIX>BuiltProjectOutputGroup%3bBuiltProjectOutputGroupDependencies%3bGetCopyToOutputDirectoryItems%3bSatelliteDllsProjectOutputGroup%3bPkgdefProjectOutputGroup%3b</IncludeOutputGroupsInVSIX>

+      <IncludeOutputGroupsInVSIXLocalOnly>DebugSymbolsProjectOutputGroup%3b</IncludeOutputGroupsInVSIXLocalOnly>

+    </ProjectReference>

+  </ItemGroup>

   <PropertyGroup>

     <UseCodebase>true</UseCodebase>

   </PropertyGroup>

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

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

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

   <PropertyGroup>

     <PreBuildEvent>copy /y "..\..\boogie\Binaries\UnivBackPred2.smt2" "$(ProjectDir)"

@@ -190,4 +199,4 @@ copy /y "..\Binaries\DafnyRuntime.cs" "$(ProjectDir)"</PreBuildEvent>
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/DafnyExtension/GlobalSuppressions.cs b/Source/DafnyExtension/GlobalSuppressions.cs
index 878ee0c3..4b115d31 100644
--- a/Source/DafnyExtension/GlobalSuppressions.cs
+++ b/Source/DafnyExtension/GlobalSuppressions.cs
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
new file mode 100644
index 00000000..69bf03d3
--- /dev/null
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -0,0 +1,109 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Threading.Tasks;

+using Microsoft.VisualStudio.Text.Editor;

+

+namespace DafnyLanguage

+{

+  class MenuProxy : DafnyLanguage.DafnyMenu.IMenuProxy

+  {

+    private DafnyMenu.DafnyMenuPackage DafnyMenuPackage;

+

+    public MenuProxy(DafnyMenu.DafnyMenuPackage DafnyMenuPackage)

+    {

+      this.DafnyMenuPackage = DafnyMenuPackage;

+    }

+

+    public bool ToggleSnapshotVerification(IWpfTextView activeTextView)

+    {

+      return DafnyDriver.ToggleIncrementalVerification();

+    }

+

+    public bool StopVerifierCommandEnabled(IWpfTextView activeTextView)

+    {

+      DafnyLanguage.ProgressTagger tagger;

+      return activeTextView != null

+                    && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)

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

+    }

+

+    public void StopVerifier(IWpfTextView activeTextView)

+    {

+      DafnyLanguage.ProgressTagger tagger;

+      if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))

+      {

+        tagger.StopVerification();

+      }

+    }

+

+    public bool RunVerifierCommandEnabled(IWpfTextView activeTextView)

+    {

+      DafnyLanguage.ProgressTagger tagger;

+      return activeTextView != null

+                 && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)

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

+    }

+

+    public void RunVerifier(IWpfTextView activeTextView)

+    {

+      DafnyLanguage.ProgressTagger tagger;

+      if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))

+      {

+        tagger.StartVerification();

+      }

+    }

+

+    public bool MenuEnabled(IWpfTextView activeTextView)

+    {

+      return activeTextView != null && activeTextView.TextBuffer.ContentType.DisplayName == "dafny";

+    }

+

+    public bool CompileCommandEnabled(IWpfTextView activeTextView)

+    {

+      ResolverTagger resolver;

+      return activeTextView != null

+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

+                    && resolver.Program != null;

+    }

+

+    public void Compile(IWpfTextView activeTextView)

+    {

+      ResolverTagger resolver;

+      if (activeTextView != null

+          && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

+          && resolver.Program != null)

+      {

+        DafnyMenuPackage.ExecuteAsCompiling(() => { DafnyDriver.Compile(resolver.Program); });

+      }

+    }

+

+    public bool ShowErrorModelCommandEnabled(IWpfTextView activeTextView)

+    {

+      ResolverTagger resolver;

+      return activeTextView != null

+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

+                    && resolver.Program != null

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

+    }

+

+    public void ShowErrorModel(IWpfTextView activeTextView)

+    {

+      ResolverTagger resolver = null;

+      var show = activeTextView != null

+                 && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

+                 && resolver.Program != null

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

+      if (show)

+      {

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

+

+        if (selectedError != null)

+        {

+          DafnyMenuPackage.ShowErrorModel(selectedError.Model, selectedError.SelectedStateId);

+        }

+      }

+    }

+  }

+}

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 9d10cb70..5d26573e 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -140,9 +140,9 @@ namespace DafnyLanguage
             {

               Microsoft.Boogie.ExecutionEngine.CancelRequest(lastRequestId);

             }

-            if (_document.FilePath != null)

+            if (_document != null && _document.TextBuffer != null)

             {

-              ProgressTaggers.Remove(_document.FilePath);

+              ProgressTaggers.Remove(_document.TextBuffer);

             }

             _buffer.Changed -= buffer_Changed;

             timer.Tick -= UponIdle;

@@ -194,7 +194,7 @@ namespace DafnyLanguage
     public bool VerificationDisabled { get; private set; }

     string lastRequestId;

 

-    public static readonly IDictionary<string, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<string, ProgressTagger>();

+    public static readonly IDictionary<ITextBuffer, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<ITextBuffer, ProgressTagger>();

 

     public readonly ConcurrentDictionary<string, ITextSnapshot> RequestIdToSnapshot = new ConcurrentDictionary<string, ITextSnapshot>();

 

@@ -245,7 +245,7 @@ namespace DafnyLanguage
 

         if (_document != null)

         {

-          ProgressTaggers[_document.FilePath] = this;

+          ProgressTaggers[_document.TextBuffer] = this;

         }

 

         verificationTask = System.Threading.Tasks.Task.Factory.StartNew(

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 380df534..dedf506a 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -208,7 +208,7 @@ namespace DafnyLanguage
       }

     }

 

-    public static readonly IDictionary<string, ResolverTagger> ResolverTaggers = new ConcurrentDictionary<string, ResolverTagger>();

+    public static readonly IDictionary<ITextBuffer, ResolverTagger> ResolverTaggers = new ConcurrentDictionary<ITextBuffer, ResolverTagger>();

 

     internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory)

     {

@@ -249,9 +249,9 @@ namespace DafnyLanguage
               _errorProvider = null;

             }

             BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);

-            if (_document != null)

+            if (_document != null && _document.TextBuffer != null)

             {

-              ResolverTaggers.Remove(_document.FilePath);

+              ResolverTaggers.Remove(_document.TextBuffer);

             }

           }

 

@@ -333,11 +333,11 @@ namespace DafnyLanguage
 

       if (program != null && _document != null)

       {

-        ResolverTaggers[_document.FilePath] = this;

+        ResolverTaggers[_document.TextBuffer] = this;

       }

       else if (_document != null)

       {

-        ResolverTaggers.Remove(_document.FilePath);

+        ResolverTaggers.Remove(_document.TextBuffer);

       }

 

       _resolutionErrors = newErrors;

diff --git a/Source/DafnyExtension/source.extension.vsixmanifest b/Source/DafnyExtension/source.extension.vsixmanifest
index ed1bbb1e..9fda1773 100644
--- a/Source/DafnyExtension/source.extension.vsixmanifest
+++ b/Source/DafnyExtension/source.extension.vsixmanifest
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="utf-8"?>

 <PackageManifest Version="2.0.0" xmlns="http://schemas.microsoft.com/developer/vsx-schema/2011" xmlns:d="http://schemas.microsoft.com/developer/vsx-schema-design/2011">

   <Metadata>

-    <Identity Id="DafnyLanguageMode.Microsoft.6c7ed99a-206a-4937-9e08-b389de175f68" Version="1.0" Language="en-US" Publisher="Microsoft Research" />

+    <Identity Id="6c7ed99a-206a-4937-9e08-b389de175f68" Version="1.0" Language="en-US" Publisher="Microsoft Research" />

     <DisplayName>DafnyLanguageMode</DisplayName>

     <Description xml:space="preserve">This is a language mode for using the Dafny language inside Visual Studio.</Description>

   </Metadata>

@@ -15,5 +15,6 @@
   <Assets>

     <Asset Type="Microsoft.VisualStudio.VsPackage" d:Source="Project" d:ProjectName="%CurrentProject%" Path="|%CurrentProject%;PkgdefProjectOutputGroup|" />

     <Asset Type="Microsoft.VisualStudio.MefComponent" d:Source="Project" d:ProjectName="%CurrentProject%" Path="|%CurrentProject%|" />

+    <Asset Type="Microsoft.VisualStudio.VsPackage" d:Source="Project" d:ProjectName="DafnyMenu" Path="|DafnyMenu;PkgdefProjectOutputGroup|" />

   </Assets>

 </PackageManifest>

diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
index 8c528f31..c3a1647b 100644
--- a/Source/DafnyMenu/DafnyMenu.csproj
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -30,9 +30,9 @@
     <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>

@@ -56,6 +56,9 @@
     </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" />

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

@@ -67,6 +70,9 @@
     <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0" />

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

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

@@ -127,12 +133,6 @@
   <ItemGroup>

     <Folder Include="Resources\" />

   </ItemGroup>

-  <ItemGroup>

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

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

-      <Name>DafnyExtension</Name>

-    </ProjectReference>

-  </ItemGroup>

   <PropertyGroup>

     <UseCodebase>true</UseCodebase>

   </PropertyGroup>

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 5481141c..7ff78c86 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}")]

@@ -41,6 +78,8 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand stopVerifierCommand;

     private OleMenuCommand toggleSnapshotVerificationCommand;

     private OleMenuCommand showErrorModelCommand;

+    public IMenuProxy MenuProxy { get; set; }

+

 

     /// <summary>

     /// Default constructor of the package.

@@ -90,7 +129,6 @@ 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);

 

@@ -108,142 +146,165 @@ 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 stopVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)

+    void RunVerifierCallback(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)

+      {

+        MenuProxy.RunVerifier(atv);

+      }

     }

 

-    void compileCommand_BeforeQueryStatus(object sender, EventArgs e)

+    void menuCommand_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 isActive = MenuProxy.MenuEnabled(atv);

+        menuCommand.Visible = isActive;

+        menuCommand.Enabled = isActive;

+      }

     }

 

-    #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 compileCommand_BeforeQueryStatus(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);

+        var enabled = MenuProxy.CompileCommandEnabled(atv);

+        compileCommand.Enabled = enabled;

+      }

+    }

 

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

+    void CompileCallback(object sender, EventArgs e)

+    {

+      var atv = ActiveTextView;

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

+      {

+        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);

+        showErrorModelCommand.Visible = visible;

+      }

     }

 

-    private void ShowErrorModelCallback(object sender, EventArgs e)

+    void ShowErrorModelCallback(object sender, EventArgs e)

     {

-      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)

+      var atv = ActiveTextView;

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

       {

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

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

-        {

-          throw new NotSupportedException("Can not create BvdToolWindow.");

-        }

+        MenuProxy.ShowErrorModel(atv);

+      }

+    }

 

-        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);

-        }

+    public void ExecuteAsCompiling(Action action)

+    {

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

+      uint cookie = 0;

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

 

-        IVsWindowFrame windowFrame = (IVsWindowFrame)window.Frame;

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

+      action();

+

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

+    }

+

+    public void ShowErrorModel(string model, int id)

+    {

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

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

+      {

+        throw new NotSupportedException("Can not create BvdToolWindow.");

       }

+

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