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

8 files changed, 141 insertions, 18 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>