Merge

8 files changed, 219 insertions, 82 deletions

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 3dc67098..08040853 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.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>

@@ -106,7 +106,9 @@
     <Reference Include="Houdini">

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

     </Reference>

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

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

+      <HintPath>..\packages\VSSDK.Language.11.0.4\lib\net45\Microsoft.VisualStudio.Language.Intellisense.dll</HintPath>

+    </Reference>

     <Reference Include="Model">

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

     </Reference>

@@ -124,23 +126,57 @@
     </Reference>

   </ItemGroup>

   <ItemGroup>

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

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

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

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

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

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

-    <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.CoreUtility, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

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

-    <Reference Include="Microsoft.VisualStudio.Text.Data, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

-    <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

-    <Reference Include="Microsoft.VisualStudio.Text.UI, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

-    <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

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

+    <Reference Include="Microsoft.VisualStudio.Shell.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">

+      <HintPath>..\packages\VSSDK.Shell.Interop.7.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Editor, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Editor.11.0.4\lib\net45\Microsoft.VisualStudio.Editor.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.ComponentModelHost, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.ComponentModelHost.11.0.4\lib\net45\Microsoft.VisualStudio.ComponentModelHost.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Shell.11.11.0.4\lib\net45\Microsoft.VisualStudio.Shell.11.0.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.Shell.Immutable.10.10.0.4\lib\net40\Microsoft.VisualStudio.Shell.Immutable.10.0.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.OLE.Interop.7.0.4\lib\net20\Microsoft.VisualStudio.OLE.Interop.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Shell.Interop.11.11.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.11.0.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.Shell.Interop.10.10.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.10.0.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.Shell.Interop.8.8.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.8.0.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.Shell.Interop.9.9.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.9.0.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.CoreUtility, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.CoreUtility.11.0.4\lib\net45\Microsoft.VisualStudio.CoreUtility.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.TextManager.Interop.7.0.4\lib\net20\Microsoft.VisualStudio.TextManager.Interop.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Text.Data, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.Data.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.Logic.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Text.UI, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.UI.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.UI.Wpf.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.Language.11.0.4\lib\net45\Microsoft.VisualStudio.Language.StandardClassification.dll</HintPath>

+    </Reference>

   </ItemGroup>

   <ItemGroup>

     <Reference Include="PresentationCore" />

@@ -200,6 +236,9 @@
     </Content>

   </ItemGroup>

   <ItemGroup>

+    <None Include="packages.config">

+      <SubType>Designer</SubType>

+    </None>

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

       <SubType>Designer</SubType>

     </None>

@@ -250,4 +289,4 @@ copy /y "..\Binaries\z3.exe" "$(ProjectDir)"</PreBuildEvent>
   <Target Name="AfterBuild">

   </Target>

   -->

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

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 22706338..b348e7d6 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -189,7 +189,7 @@ namespace DafnyLanguage
     {

       get

       {

-        return _verificationErrors.Values.Where(ec => ec.RequestId == MostRecentRequestId).SelectMany(ec => ec.Errors.Reverse());

+        return _verificationErrors.Values.Where(ec => ec.RequestId == MostRecentRequestId).SelectMany(ec => ec.Errors.Reverse()).ToList();

       }

     }

 

@@ -354,49 +354,46 @@ namespace DafnyLanguage
 

     public void UpdateErrorList(ITextSnapshot snapshot)

     {

-      lock (this) 

+      if (_errorProvider != null && !m_disposed)

       {

-        if (_errorProvider != null && !m_disposed)

-        {

-          _errorProvider.SuspendRefresh();  // reduce flickering

-          _errorProvider.Tasks.Clear();

-          foreach (var err in AllErrors)

-          { 

-            var lineNum = 0;

-            var columnNum = 0;

-            if (err.Span != null) {

-              var span = err.Span.GetSpan(snapshot);

-              lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);

-              var line = snapshot.GetLineFromPosition(span.Start.Position);

-              columnNum = span.Start - line.Start;

-            } else {

-              lineNum = err.Line;

-              columnNum = err.Column;

-            }

-            

-            ErrorTask task = new ErrorTask()

-            {

-              Category = TaskCategory.BuildCompile,

-              ErrorCategory = CategoryConversion(err.Category),

-              Text = err.Message,

-              Line = lineNum,

-              Column = columnNum

-            };

-            if (err.Filename != null) {

-              task.Document = err.Filename;

-            } 

-            else if (_document != null)

-            {

-              task.Document = _document.FilePath;

-            }

-            if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)

-            {

-              task.Navigate += new EventHandler(NavigateHandler);

-            }

-            _errorProvider.Tasks.Add(task);

+        _errorProvider.SuspendRefresh();  // reduce flickering

+        _errorProvider.Tasks.Clear();

+        foreach (var err in AllErrors)

+        { 

+          var lineNum = 0;

+          var columnNum = 0;

+          if (err.Span != null) {

+            var span = err.Span.GetSpan(snapshot);

+            lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);

+            var line = snapshot.GetLineFromPosition(span.Start.Position);

+            columnNum = span.Start - line.Start;

+          } else {

+            lineNum = err.Line;

+            columnNum = err.Column;

+          }

+          

+          ErrorTask task = new ErrorTask()

+          {

+            Category = TaskCategory.BuildCompile,

+            ErrorCategory = CategoryConversion(err.Category),

+            Text = err.Message,

+            Line = lineNum,

+            Column = columnNum

+          };

+          if (err.Filename != null) {

+            task.Document = err.Filename;

+          } 

+          else if (_document != null)

+          {

+            task.Document = _document.FilePath;

+          }

+          if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)

+          {

+            task.Navigate += new EventHandler(NavigateHandler);

           }

-          _errorProvider.ResumeRefresh();

+          _errorProvider.Tasks.Add(task);

         }

+        _errorProvider.ResumeRefresh();

       }

       var chng = TagsChanged;

       if (chng != null)

diff --git a/Source/DafnyExtension/packages.config b/Source/DafnyExtension/packages.config
new file mode 100644
index 00000000..60f856c5
--- /dev/null
+++ b/Source/DafnyExtension/packages.config
@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="utf-8"?>

+<packages>

+  <package id="VSSDK.ComponentModelHost" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.ComponentModelHost.11" version="11.0.3" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.CoreUtility" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.CoreUtility.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.DTE" version="7.0.4" targetFramework="net45" />

+  <package id="VSSDK.Editor" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.IDE" version="7.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.IDE.10" version="10.0.4" targetFramework="net45" />

+  <package id="VSSDK.IDE.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.IDE.8" version="8.0.4" targetFramework="net45" />

+  <package id="VSSDK.IDE.9" version="9.0.4" targetFramework="net45" />

+  <package id="VSSDK.Language" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.Language.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.OLE.Interop" version="7.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.Shell.Immutable.10" version="10.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Immutable.11" version="11.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop" version="7.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop.10" version="10.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop.11" version="11.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop.8" version="8.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop.9" version="9.0.4" targetFramework="net45" />

+  <package id="VSSDK.Text" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.Text.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.TextManager.Interop" version="7.0.4" targetFramework="net45" />

+  <package id="VSSDK.TextManager.Interop.8" version="8.0.4" targetFramework="net45" />

+</packages>

diff --git a/Source/DafnyExtension/source.extension.vsixmanifest b/Source/DafnyExtension/source.extension.vsixmanifest
index b87e2452..66e4deda 100644
--- a/Source/DafnyExtension/source.extension.vsixmanifest
+++ b/Source/DafnyExtension/source.extension.vsixmanifest
@@ -7,7 +7,8 @@
     <License>Z3-LICENSE.txt</License>

   </Metadata>

   <Installation InstalledByMsi="false">

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

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

+    <InstallationTarget Version="[14.0,15.0)" Id="Microsoft.VisualStudio.Community" />

   </Installation>

   <Dependencies>

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

diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
index 503b3d0c..2a222038 100644
--- a/Source/DafnyMenu/DafnyMenu.csproj
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -62,22 +62,50 @@
   </ItemGroup>

   <ItemGroup>

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

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

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

-    <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

+    <Reference Include="Microsoft.VisualStudio.Editor, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Editor.11.0.4\lib\net45\Microsoft.VisualStudio.Editor.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.ComponentModelHost, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.ComponentModelHost.11.0.4\lib\net45\Microsoft.VisualStudio.ComponentModelHost.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Shell.11.11.0.4\lib\net45\Microsoft.VisualStudio.Shell.11.0.dll</HintPath>

+    </Reference>

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

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

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

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

-    <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.CoreUtility, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

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

+      <HintPath>..\packages\VSSDK.OLE.Interop.7.0.4\lib\net20\Microsoft.VisualStudio.OLE.Interop.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Shell.Interop.11.11.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.11.0.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.Shell.Interop.10.10.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.10.0.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.Shell.Interop.8.8.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.8.0.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.Shell.Interop.9.9.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.9.0.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.CoreUtility, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.CoreUtility.11.0.4\lib\net45\Microsoft.VisualStudio.CoreUtility.dll</HintPath>

+    </Reference>

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

-    <Reference Include="Microsoft.VisualStudio.Text.Data, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

-    <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

-    <Reference Include="Microsoft.VisualStudio.Text.UI, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

-    <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

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

+    <Reference Include="Microsoft.VisualStudio.Text.Data, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.Data.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.Logic.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Text.UI, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.UI.dll</HintPath>

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

+      <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.UI.Wpf.dll</HintPath>

+    </Reference>

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

+      <HintPath>..\packages\VSSDK.Language.11.0.4\lib\net45\Microsoft.VisualStudio.Language.StandardClassification.dll</HintPath>

+    </Reference>

   </ItemGroup>

   <ItemGroup>

     <Reference Include="PresentationCore" />

@@ -127,6 +155,9 @@
     </EmbeddedResource>

   </ItemGroup>

   <ItemGroup>

+    <None Include="packages.config">

+      <SubType>Designer</SubType>

+    </None>

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

       <SubType>Designer</SubType>

     </None>

diff --git a/Source/DafnyMenu/packages.config b/Source/DafnyMenu/packages.config
new file mode 100644
index 00000000..60f856c5
--- /dev/null
+++ b/Source/DafnyMenu/packages.config
@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="utf-8"?>

+<packages>

+  <package id="VSSDK.ComponentModelHost" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.ComponentModelHost.11" version="11.0.3" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.CoreUtility" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.CoreUtility.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.DTE" version="7.0.4" targetFramework="net45" />

+  <package id="VSSDK.Editor" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.IDE" version="7.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.IDE.10" version="10.0.4" targetFramework="net45" />

+  <package id="VSSDK.IDE.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.IDE.8" version="8.0.4" targetFramework="net45" />

+  <package id="VSSDK.IDE.9" version="9.0.4" targetFramework="net45" />

+  <package id="VSSDK.Language" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.Language.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.OLE.Interop" version="7.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.Shell.Immutable.10" version="10.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Immutable.11" version="11.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop" version="7.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop.10" version="10.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop.11" version="11.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop.8" version="8.0.4" targetFramework="net45" />

+  <package id="VSSDK.Shell.Interop.9" version="9.0.4" targetFramework="net45" />

+  <package id="VSSDK.Text" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.Text.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />

+  <package id="VSSDK.TextManager.Interop" version="7.0.4" targetFramework="net45" />

+  <package id="VSSDK.TextManager.Interop.8" version="8.0.4" targetFramework="net45" />

+</packages>

diff --git a/Source/DafnyMenu/source.extension.vsixmanifest b/Source/DafnyMenu/source.extension.vsixmanifest
index 7beeb69e..814374ee 100644
--- a/Source/DafnyMenu/source.extension.vsixmanifest
+++ b/Source/DafnyMenu/source.extension.vsixmanifest
@@ -6,7 +6,8 @@
     <Description xml:space="preserve">This is a menu for interacting with Dafny.</Description>

   </Metadata>

   <Installation InstalledByMsi="false">

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

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

+    <InstallationTarget Version="[14.0,15.0)" Id="Microsoft.VisualStudio.Community" />

   </Installation>

   <Dependencies>

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

diff --git a/package.py b/package.py
index 33e83d73..32192822 100644..100755
--- a/package.py
+++ b/package.py
@@ -1,12 +1,14 @@
+#!/usr/bin/env python3
+
 from fnmatch import fnmatch
 from os import path
 import argparse
 import json
 import os
 import re
-import shutil
 import subprocess
 import sys
+import time
 import urllib.request
 import zipfile
 
@@ -53,7 +55,7 @@ DLLs = ["AbsInt",
         "VCExpr",
         "VCGeneration"]
 EXEs = ["Dafny", "DafnyServer"]
-ETCs = ["dafny", "DafnyPrelude.bpl", "DafnyRuntime.cs"]
+ETCs = ["dafny", "DafnyPrelude.bpl", "DafnyRuntime.cs", "DafnyLanguageService.vsix"]
 
 # Constants
 
@@ -112,6 +114,11 @@ class Release:
                     writer.write(reader.read())
             flush("done!")
 
+    @staticmethod
+    def zipify_path(fpath):
+        """Zip entries always use '/' as the path separator."""
+        return fpath.replace(os.path.sep, '/')
+
     def pack(self):
         try:
             os.remove(self.dafny_zip)
@@ -126,16 +133,19 @@ class Release:
                     if any(fnmatch(fname, pattern) for pattern in Z3_INTERESTING_FILES):
                         z3_files_count += 1
                         contents = Z3_archive.read(fileinfo)
-                        fileinfo.filename = path.join(DAFNY_PACKAGE_PREFIX, Z3_PACKAGE_PREFIX, fname)
+                        fileinfo.filename = Release.zipify_path(path.join(DAFNY_PACKAGE_PREFIX, Z3_PACKAGE_PREFIX, fname))
                         archive.writestr(fileinfo, contents)
             for fname in ARCHIVE_FNAMES:
                 fpath = path.join(BINARIES_DIRECTORY, fname)
                 if path.exists(fpath):
-                    fileinfo = zipfile.ZipInfo(fname)
+                    fileinfo = zipfile.ZipInfo(fname, time.localtime(os.stat(fpath).st_mtime)[:6])
                     if any(fnmatch(fname, pattern) for pattern in UNIX_EXECUTABLES):
                         # http://stackoverflow.com/questions/434641/
                         fileinfo.external_attr = 0o777 << 16
-                    archive.write(fpath, path.join(DAFNY_PACKAGE_PREFIX, fname))
+                    contents = open(fpath, mode='rb').read()
+                    fileinfo.compress_type = zipfile.ZIP_DEFLATED
+                    fileinfo.filename = Release.zipify_path(path.join(DAFNY_PACKAGE_PREFIX, fname))
+                    archive.writestr(fileinfo, contents)
                 else:
                     missing.append(fname)
         flush("done! (imported {} files from z3's sources)".format(z3_files_count))