DafnyExtension: Did some refactoring and worked towards integrating the Dafny menu more tightly.

1 files changed, 83 insertions, 134 deletions

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index a46feec3..4a2a336a 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -1,29 +1,26 @@
-<?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>

+    <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,114 +46,100 @@
     <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" />

@@ -213,32 +167,27 @@
     <Content Include="DafnyRuntime.cs">

       <IncludeInVSIX>true</IncludeInVSIX>

     </Content>

+  </ItemGroup>

+  <ItemGroup>

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

       <SubType>Designer</SubType>

     </None>

   </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="$(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>

   <Target Name="AfterBuild">

   </Target>

   -->

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