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

3 files changed, 167 insertions, 112 deletions

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