From 430176aab231e6105dc4e2483566aae1438a7634 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 15 Nov 2011 19:16:47 -0800
Subject: DafnyExtension: fixed build problems

---
 Source/Dafny/Resolver.cs                                      |  7 ++++++-
 Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs      |  9 ++++-----
 .../DafnyExtension/DafnyExtension/DafnyExtension.csproj       | 11 -----------
 3 files changed, 10 insertions(+), 17 deletions(-)

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 81216f32..55c2f48b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -12,7 +12,12 @@ using Microsoft.Boogie;
 namespace Microsoft.Dafny {
   public class Resolver {
     public int ErrorCount = 0;
-    void Error(IToken tok, string msg, params object[] args) {
+    public virtual void HereIsASillyTest() {
+    }
+    /// <summary>
+    /// This method is virtual, because it is overridden in the VSX plug-in for Dafny.
+    /// </summary>
+    protected virtual void Error(IToken tok, string msg, params object[] args) {
       Contract.Requires(tok != null);
       Contract.Requires(msg != null);
       ConsoleColor col = Console.ForegroundColor;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index 3c2393bb..19a5e1df 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -7,7 +7,7 @@ using System.Diagnostics;
 using System.Diagnostics.Contracts;
 // Here come the Dafny/Boogie specific imports
 //using PureCollections;
-using Microsoft.Boogie;
+using Bpl = Microsoft.Boogie;
 using Dafny = Microsoft.Dafny;
 using Microsoft.Boogie.AbstractInterpretation;
 using VC;
@@ -112,10 +112,9 @@ namespace DafnyLanguage
     }
 
     static void Initialize() {
-      CommandLineOptions.Clo.RunningBoogieOnSsc = false;
-      CommandLineOptions.Clo.TheProverFactory = ProverFactory.Load("Z3");
-      CommandLineOptions.Clo.ProverName = "Z3";
-      CommandLineOptions.Clo.vcVariety = CommandLineOptions.Clo.TheProverFactory.DefaultVCVariety;
+      if (Dafny.DafnyOptions.O == null) {
+        Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());
+      }
     }
 
     public Dafny.Program Process() {
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index 55f2ee34..4ae02e17 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -76,14 +76,6 @@
       <SpecificVersion>False</SpecificVersion>
       <HintPath>..\..\..\..\Binaries\VCGeneration.dll</HintPath>
     </Reference>
-    <Reference Include="System.Compiler, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
-      <SpecificVersion>False</SpecificVersion>
-      <HintPath>..\..\Binaries\System.Compiler.dll</HintPath>
-    </Reference>
-    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
-      <SpecificVersion>False</SpecificVersion>
-      <HintPath>..\..\Binaries\System.Compiler.Runtime.dll</HintPath>
-    </Reference>
     <Reference Include="EnvDTE, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
       <EmbedInteropTypes>False</EmbedInteropTypes>
     </Reference>
@@ -130,8 +122,6 @@
   </ItemGroup>
   <ItemGroup>
     <Compile Include="BufferIdleEventUtil.cs" />
-    <Compile Include="Visitor.cs" />
-    <Compile Include="IdentifierTagger.cs" />
     <Compile Include="OutliningTagger.cs" />
     <Compile Include="ResolverTagger.cs" />
     <Compile Include="DafnyDriver.cs" />
@@ -145,7 +135,6 @@
     <Compile Include="Properties\AssemblyInfo.cs" />
   </ItemGroup>
   <ItemGroup>
-    <None Include="app.config" />
     <None Include="source.extension.vsixmanifest">
       <SubType>Designer</SubType>
     </None>
-- 
cgit v1.2.3