Merge

20 files changed, 473 insertions, 338 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 3cdb7bbf..71dec0d7 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -414,7 +414,7 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t
 = (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

      Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);

      Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);

-     string name = null;  isGhost = false; .)

+     string name = null; id = Token.NoToken; ty = null; isGhost = false; .)

   [ "ghost"                            (. isGhost = true; .)

   ]

   ( TypeAndToken<out id, out ty>

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 9e802eb1..74f7dae6 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

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

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

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

@@ -126,12 +126,10 @@
     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

   <ItemGroup>

-    <Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

+    <Reference Include="Basetypes">

       <HintPath>..\..\..\boogie\Binaries\Basetypes.dll</HintPath>

     </Reference>

-    <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

+    <Reference Include="Core">

       <HintPath>..\..\..\boogie\Binaries\Core.dll</HintPath>

     </Reference>

     <Reference Include="ParserHelper">

@@ -193,4 +191,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

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

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index e888dac9..daf3763c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -984,7 +984,7 @@ bool IsParenStar() {
 		Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

 		Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);

 		Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);

-		string name = null;  isGhost = false; 

+		string name = null; id = Token.NoToken; ty = null; isGhost = false; 

 		if (la.kind == 22) {

 			Get();

 			isGhost = true; 

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index a62786fe..94794cd2 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

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

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

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

@@ -133,8 +133,7 @@
     <Reference Include="ExecutionEngine">

       <HintPath>..\..\..\boogie\Binaries\ExecutionEngine.dll</HintPath>

     </Reference>

-    <Reference Include="ParserHelper, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

+    <Reference Include="ParserHelper">

       <HintPath>..\..\..\boogie\Binaries\ParserHelper.dll</HintPath>

     </Reference>

     <Reference Include="Provers.SMTLib">

@@ -186,4 +185,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

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

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 a46feec3..31e344a1 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -1,29 +1,26 @@
 <?xml version="1.0" encoding="utf-8"?>

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

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

+    <VSToolsPath Condition="'$(VSToolsPath)' == ''">$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion)</VSToolsPath>

+    <TargetFrameworkProfile />

+  </PropertyGroup>

   <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

     <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

-    <ProductVersion>10.0.20305</ProductVersion>

     <SchemaVersion>2.0</SchemaVersion>

-    <ProjectTypeGuids>{82b43b9b-a64c-4715-b499-d71e9ca2bd60};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}</ProjectTypeGuids>

     <ProjectGuid>{6E9A5E14-0763-471C-A129-80A879D9E7BA}</ProjectGuid>

+    <ProjectTypeGuids>{82b43b9b-a64c-4715-b499-d71e9ca2bd60};{60dc8134-eba5-43b8-bcc9-bb4bc16c2548};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}</ProjectTypeGuids>

     <OutputType>Library</OutputType>

     <AppDesignerFolder>Properties</AppDesignerFolder>

     <RootNamespace>DafnyLanguage</RootNamespace>

     <AssemblyName>DafnyLanguageService</AssemblyName>

+    <SignAssembly>false</SignAssembly>

+    <AssemblyOriginatorKeyFile>

+    </AssemblyOriginatorKeyFile>

     <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>

-    <FileAlignment>512</FileAlignment>

-    <GeneratePkgDefFile>false</GeneratePkgDefFile>

-    <MinimumVisualStudioVersion>11.0</MinimumVisualStudioVersion>

-    <FileUpgradeFlags>

-    </FileUpgradeFlags>

-    <UpgradeBackupLocation>

-    </UpgradeBackupLocation>

-    <OldToolsVersion>4.0</OldToolsVersion>

-    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

-    <TargetFrameworkProfile>

-    </TargetFrameworkProfile>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

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

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

-    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

-    <CodeContractsInferRequires>False</CodeContractsInferRequires>

-    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>

-    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>

-    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>

-    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>

-    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>

-    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly />

-    <CodeContractsCustomRewriterClass />

-    <CodeContractsLibPaths />

-    <CodeContractsExtraRewriteOptions />

-    <CodeContractsExtraAnalysisOptions />

-    <CodeContractsBaseLineFile />

-    <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

-    <Prefer32Bit>false</Prefer32Bit>

-    <CopyVsixExtensionFiles>False</CopyVsixExtensionFiles>

-    <CopyVsixExtensionLocation>

-    </CopyVsixExtensionLocation>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <Prefer32Bit>false</Prefer32Bit>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <CreateVsixContainer>True</CreateVsixContainer>

+    <DeployExtension>True</DeployExtension>

+    <CopyVsixExtensionFiles>false</CopyVsixExtensionFiles>

+    <GeneratePkgDefFile>false</GeneratePkgDefFile>

+    <CopyVsixManifestToOutput>false</CopyVsixManifestToOutput>

   </PropertyGroup>

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

     <DebugType>pdbonly</DebugType>

@@ -78,119 +46,106 @@
     <DefineConstants>TRACE</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

+    <RunCodeAnalysis>true</RunCodeAnalysis>

     <Prefer32Bit>false</Prefer32Bit>

   </PropertyGroup>

   <ItemGroup>

-    <Reference Include="AbsInt, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

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

+    <Reference Include="AbsInt">

+      <HintPath>..\..\Binaries\AbsInt.dll</HintPath>

     </Reference>

-    <Reference Include="Basetypes, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

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

+    <Reference Include="Basetypes">

+      <HintPath>..\..\Binaries\Basetypes.dll</HintPath>

     </Reference>

-    <Reference Include="CodeContractsExtender, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

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

+    <Reference Include="CodeContractsExtender">

+      <HintPath>..\..\Binaries\CodeContractsExtender.dll</HintPath>

     </Reference>

-    <Reference Include="Core, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

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

+    <Reference Include="Core">

+      <HintPath>..\..\Binaries\Core.dll</HintPath>

     </Reference>

-    <Reference Include="Dafny, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+    <Reference Include="Dafny">

       <HintPath>..\..\Binaries\Dafny.exe</HintPath>

-      <SpecificVersion>False</SpecificVersion>

     </Reference>

-    <Reference Include="DafnyPipeline, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

+    <Reference Include="DafnyPipeline">

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

     </Reference>

-    <Reference Include="Doomed, Version=0.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

+    <Reference Include="Doomed">

       <HintPath>..\..\..\boogie\Binaries\Doomed.dll</HintPath>

     </Reference>

-    <Reference Include="EnvDTE, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">

-      <EmbedInteropTypes>False</EmbedInteropTypes>

-    </Reference>

-    <Reference Include="ExecutionEngine, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

+    <Reference Include="ExecutionEngine">

       <HintPath>..\..\..\boogie\Binaries\ExecutionEngine.dll</HintPath>

     </Reference>

-    <Reference Include="Graph, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

+    <Reference Include="Graph">

       <HintPath>..\..\..\boogie\Binaries\Graph.dll</HintPath>

     </Reference>

-    <Reference Include="Houdini, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

+    <Reference Include="Houdini">

       <HintPath>..\..\..\boogie\Binaries\Houdini.dll</HintPath>

     </Reference>

-    <Reference Include="Microsoft.VisualStudio.CoreUtility">

-      <Private>False</Private>

-    </Reference>

-    <Reference Include="Microsoft.VisualStudio.Language.Intellisense, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-    </Reference>

-    <Reference Include="Microsoft.VisualStudio.Language.StandardClassification, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-    </Reference>

-    <Reference Include="Microsoft.VisualStudio.OLE.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />

-    <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.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />

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

-      <EmbedInteropTypes>True</EmbedInteropTypes>

+    <Reference Include="Graph">

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

     </Reference>

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

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

-    <Reference Include="Microsoft.VisualStudio.Text.Data">

-      <Private>False</Private>

+    <Reference Include="Model">

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

     </Reference>

-    <Reference Include="Microsoft.VisualStudio.Text.Logic">

-      <Private>False</Private>

+    <Reference Include="ParserHelper">

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

     </Reference>

-    <Reference Include="Microsoft.VisualStudio.Text.UI">

-      <Private>False</Private>

+    <Reference Include="Provers.SMTLib">

+      <HintPath>..\..\..\boogie\Binaries\Provers.SMTLib.dll</HintPath>

     </Reference>

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

-      <Private>False</Private>

+    <Reference Include="VCExpr">

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

     </Reference>

-    <Reference Include="Microsoft.VisualStudio.TextManager.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />

-    <Reference Include="Model, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

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

+    <Reference Include="VCGeneration">

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

     </Reference>

-    <Reference Include="ParserHelper, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

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

+  </ItemGroup>

+  <ItemGroup>

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

+    <Reference Include="Microsoft.VisualStudio.Language.Intellisense" />

+    <Reference Include="Microsoft.VisualStudio.Language.StandardClassification" />

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

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

+      <EmbedInteropTypes>True</EmbedInteropTypes>

     </Reference>

+    <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.Data" />

+    <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="Provers.SMTLib, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\..\boogie\Binaries\Provers.SMTLib.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

-    <Reference Include="System.ComponentModel.Composition, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-    </Reference>

+    <Reference Include="System.ComponentModel.Composition" />

     <Reference Include="System.Core" />

     <Reference Include="System.Xaml" />

-    <Reference Include="VCExpr, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

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

-    </Reference>

-    <Reference Include="VCGeneration, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

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

-    </Reference>

     <Reference Include="WindowsBase" />

   </ItemGroup>

   <ItemGroup>

+    <COMReference Include="EnvDTE">

+      <Guid>{80CC9F66-E7D8-4DDD-85B6-D9E6CD0E93E2}</Guid>

+      <VersionMajor>8</VersionMajor>

+      <VersionMinor>0</VersionMinor>

+      <Lcid>0</Lcid>

+      <WrapperTool>primary</WrapperTool>

+      <Isolated>False</Isolated>

+      <EmbedInteropTypes>False</EmbedInteropTypes>

+    </COMReference>

+  </ItemGroup>

+  <ItemGroup>

     <Compile Include="BufferIdleEventUtil.cs" />

     <Compile Include="ErrorModelTagger.cs" />

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

@@ -213,28 +168,31 @@
     <Content Include="DafnyRuntime.cs">

       <IncludeInVSIX>true</IncludeInVSIX>

     </Content>

+  </ItemGroup>

+  <ItemGroup>

     <None Include="source.extension.vsixmanifest">

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

-    <VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">10.0</VisualStudioVersion>

-    <VSToolsPath Condition="'$(VSToolsPath)' == ''">$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion)</VSToolsPath>

+    <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)' != ''" />

-  <Import Project="$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" Condition="false" />

-  <PropertyGroup>

-    <PostBuildEvent>cd</PostBuildEvent>

-    <PostBuildEvent>

-    </PostBuildEvent>

-  </PropertyGroup>

   <PropertyGroup>

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

 copy /y "..\Binaries\DafnyPrelude.bpl" "$(ProjectDir)"

 copy /y "..\Binaries\DafnyRuntime.cs" "$(ProjectDir)"</PreBuildEvent>

   </PropertyGroup>

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

diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs
index acb8ccb0..781814b2 100644
--- a/Source/DafnyExtension/ErrorModelTagger.cs
+++ b/Source/DafnyExtension/ErrorModelTagger.cs
@@ -1,6 +1,7 @@
 using System;

 using System.Collections.Generic;

 using System.ComponentModel.Composition;

+using System.Linq;

 using System.Windows;

 using System.Windows.Controls;

 using System.Windows.Input;

@@ -125,20 +126,22 @@ namespace DafnyLanguage
       foreach (var adornments in adornmentsPerSnapshot)

       {

         var panel = _view.VisualElement.Dispatcher.Invoke(() =>

+        {

+          var maxConcurrentAdornments = adornments.Value.Where(a => a.Fill == Brushes.Crimson).Count()    // number of error adornments

+                                        + (adornments.Value.Any(a => a.Fill != Brushes.Crimson) ? 1 : 0); // number of error state adornments

+          var p = new StackPanel

+          {

+            Orientation = Orientation.Horizontal,

+            Width = 12.0 * maxConcurrentAdornments,

+            Height = 12.0,

+          };

+          foreach (var adornment in adornments.Value)

           {

-            var p = new StackPanel

-            {

-              Orientation = Orientation.Horizontal,

-              Width = 12.0 * adornments.Value.Count,

-              Height = 12.0,

-            };

-            foreach (var adornment in adornments.Value)

-            {

-              p.Children.Add(adornment);

-            }

-            p.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));

-            return p;

-          });

+            p.Children.Add(adornment);

+          }

+          p.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));

+          return p;

+        });

 

         yield return new TagSpan<IntraTextAdornmentTag>(adornments.Key, new IntraTextAdornmentTag(panel, null, PositionAffinity.Successor));

       }

@@ -148,12 +151,12 @@ namespace DafnyLanguage
     {

       var result = new Ellipse

       {

-        Fill = Brushes.Blue,

+        Fill = Brushes.DodgerBlue,

         Height = 12.0,

         Width = 12.0,

         ToolTip = "select state",

         StrokeThickness = 3.0,

-        Stroke = Brushes.Blue,

+        Stroke = Brushes.DodgerBlue,

         Cursor = Cursors.Arrow,

         Visibility = System.Windows.Visibility.Collapsed

       };

@@ -171,7 +174,7 @@ namespace DafnyLanguage
           // unselect it

           esrtag.Error.SelectedStateAdornment = null;

           esrtag.Error.SelectedStateId = 0;

-          result.Stroke = Brushes.Blue;

+          result.Stroke = Brushes.DodgerBlue;

           result.ToolTip = "select state";

         }

         else

@@ -179,7 +182,7 @@ namespace DafnyLanguage
           // unselect the old one

           if (esrtag.Error.SelectedStateAdornment != null)

           {

-            esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Blue;

+            esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue;

             esrtag.Error.SelectedStateAdornment.ToolTip = "select state";

             esrtag.Error.SelectedStateAdornment = null;

             esrtag.Error.SelectedStateId = 0;

@@ -190,6 +193,10 @@ namespace DafnyLanguage
           esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black;

           esrtag.Error.SelectedStateAdornment.ToolTip = "unselect state";

           esrtag.Error.SelectedStateId = esrtag.Id;

+          if (!string.IsNullOrEmpty(esrtag.Error.Model))

+          {

+            DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.Model, esrtag.Id);

+          }

         }

       });

       return result;

@@ -199,12 +206,12 @@ namespace DafnyLanguage
     {

       var result = new Ellipse

       {

-        Fill = Brushes.Red,

+        Fill = Brushes.Crimson,

         Height = 12.0,

         Width = 12.0,

         ToolTip = "select error",

         StrokeThickness = 3.0,

-        Stroke = Brushes.Red,

+        Stroke = Brushes.Crimson,

         Cursor = Cursors.Arrow,

       };

       result.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));

@@ -216,7 +223,7 @@ namespace DafnyLanguage
           var selErr = ertag.Error.SelectedError;

           ertag.Error.SelectedError = null;

           selErr.Notify();

-          result.Stroke = Brushes.Red;

+          result.Stroke = Brushes.Crimson;

           result.ToolTip = "select error";

         }

         else

@@ -225,7 +232,7 @@ namespace DafnyLanguage
           if (ertag.Error.SelectedError != null)

           {

             var selErr = ertag.Error.SelectedError;

-            selErr.Adornment.Stroke = Brushes.Red;

+            selErr.Adornment.Stroke = Brushes.Crimson;

             selErr.Adornment.ToolTip = "select error";

             ertag.Error.SelectedError = null;

             selErr.Notify();

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..fc0c0d1d
--- /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.ShowErrorModelInBVD(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/Properties/AssemblyInfo.cs b/Source/DafnyExtension/Properties/AssemblyInfo.cs
index b73b8410..a9922c2f 100644
--- a/Source/DafnyExtension/Properties/AssemblyInfo.cs
+++ b/Source/DafnyExtension/Properties/AssemblyInfo.cs
@@ -1,15 +1,14 @@
 using System.Reflection;

-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("EditorClassifier1")]

+[assembly: AssemblyTitle("DafnyLanguageService")]

 [assembly: AssemblyDescription("")]

 [assembly: AssemblyConfiguration("")]

-[assembly: AssemblyCompany("")]

-[assembly: AssemblyProduct("EditorClassifier1")]

+[assembly: AssemblyCompany("Microsoft Research")]

+[assembly: AssemblyProduct("DafnyLanguageService")]

 [assembly: AssemblyCopyright("")]

 [assembly: AssemblyTrademark("")]

 [assembly: AssemblyCulture("")]

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index ece6da50..dedf506a 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -64,12 +64,12 @@ namespace DafnyLanguage
     public DafnyError Error { get; private set; }

 

     public DafnyErrorResolverTag(DafnyError error)

-      : base(ErrorType(error), error.Message)

+      : base(ConvertToErrorType(error), error.Message)

     {

       Error = error;

     }

     

-    private static string ErrorType(DafnyError err)

+    private static string ConvertToErrorType(DafnyError err)

     {

       string ty;  // the COLORs below indicate what I see on my machine

       switch (err.Category)

@@ -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 9b4feb14..9fda1773 100644
--- a/Source/DafnyExtension/source.extension.vsixmanifest
+++ b/Source/DafnyExtension/source.extension.vsixmanifest
@@ -1,23 +1,20 @@
-<?xml version="1.0" encoding="utf-8"?>

-<Vsix xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema" Version="1.0.0" xmlns="http://schemas.microsoft.com/developer/vsx-schema/2010">

-  <Identifier Id="DafnyLanguageMode.Microsoft.6c7ed99a-206a-4937-9e08-b389de175f68">

-    <Name>DafnyLanguageMode</Name>

-    <Author>Microsoft Research</Author>

-    <Version>1.0</Version>

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

-    <Locale>1033</Locale>

-    <SupportedProducts>

-      <VisualStudio Version="11.0">

-        <Edition>Pro</Edition>

-      </VisualStudio>

-    </SupportedProducts>

-    <SupportedFrameworkRuntimeEdition MinVersion="4.0" MaxVersion="4.0" />

-  </Identifier>

-  <References />

-  <Content>

-    <MefComponent>|%CurrentProject%|</MefComponent>

-    <VsPackage>DafnyMenu</VsPackage>

-    <CustomExtension Type="Boogie">DafnyPrelude.bpl</CustomExtension>

-    <CustomExtension Type="SMTLib 2">UnivBackPred2.smt2</CustomExtension>

-  </Content>

-</Vsix>

+  </Metadata>

+  <Installation InstalledByMsi="false">

+    <InstallationTarget Version="[11.0,12.0)" Id="Microsoft.VisualStudio.Pro" />

+  </Installation>

+  <Dependencies>

+    <Dependency Id="Microsoft.Framework.NDP" DisplayName="Microsoft .NET Framework" d:Source="Manual" Version="4.5" />

+    <Dependency Id="Microsoft.VisualStudio.MPF.11.0" DisplayName="Visual Studio MPF 11.0" d:Source="Installed" Version="11.0" />

+  </Dependencies>

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