From b10153f3d755048dbce2fadf9996fc73c279fc7c Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 8 Aug 2012 21:57:20 -0700
Subject: DafnyExtension:  fixed build issues; added support for some
 refinement features

---
 .../DafnyExtension/DafnyExtension.csproj           |  8 ++++++--
 .../DafnyExtension/OutliningTagger.cs              | 23 +++++++++++++++++++---
 .../DafnyExtension/source.extension.vsixmanifest   |  2 ++
 3 files changed, 28 insertions(+), 5 deletions(-)

(limited to 'Util')

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index e978f696..62413d03 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -143,15 +143,15 @@
   </ItemGroup>
   <ItemGroup>
     <Content Include="DafnyPrelude.bpl">
-      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
       <IncludeInVSIX>true</IncludeInVSIX>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
     </Content>
     <None Include="source.extension.vsixmanifest">
       <SubType>Designer</SubType>
     </None>
     <Content Include="UnivBackPred2.smt2">
-      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
       <IncludeInVSIX>true</IncludeInVSIX>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
     </Content>
   </ItemGroup>
   <ItemGroup>
@@ -164,6 +164,10 @@
     <PostBuildEvent>
     </PostBuildEvent>
   </PropertyGroup>
+  <PropertyGroup>
+    <PreBuildEvent>copy ..\..\..\..\..\..\Binaries\DafnyPrelude.bpl $(ProjectDir)
+copy ..\..\..\..\..\..\Binaries\UnivBackPred2.smt2 $(ProjectDir)</PreBuildEvent>
+  </PropertyGroup>
   <!-- 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">
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
index 3dcaf1cf..8cbdb9f6 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
@@ -119,8 +119,17 @@ namespace DafnyLanguage
           newRegions.Add(new ORegion(module, "module"));
         }
         foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {
-          if (d is Dafny.DatatypeDecl) {
+          if (!HasBodyTokens(d)) {
+            continue;
+          }
+          if (d is Dafny.ArbitraryTypeDecl) {
+            newRegions.Add(new ORegion(d, "type"));
+          } else if (d is Dafny.CoDatatypeDecl) {
+            newRegions.Add(new ORegion(d, "codatatype"));
+          } else if (d is Dafny.DatatypeDecl) {
             newRegions.Add(new ORegion(d, "datatype"));
+          } else if (d is Dafny.ModuleDecl) {
+            // do nothing here, since the outer loop handles modules
           } else {
             Dafny.ClassDecl cl = (Dafny.ClassDecl)d;
             if (!cl.IsDefaultClass) {
@@ -128,10 +137,13 @@ namespace DafnyLanguage
             }
             // do the class members (in particular, functions and methods)
             foreach (Dafny.MemberDecl m in cl.Members) {
+              if (!HasBodyTokens(m)) {
+                continue;
+              }
               if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {
-                newRegions.Add(new ORegion(m, "function"));
+                newRegions.Add(new ORegion(m, m is Dafny.CoPredicate ? "copredicate" : m is Dafny.Predicate ? "predicate" : "function"));
               } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {
-                newRegions.Add(new ORegion(m, "method"));
+                newRegions.Add(new ORegion(m, m is Dafny.Constructor ? "constructor" : "method"));
               }
             }
           }
@@ -143,6 +155,11 @@ namespace DafnyLanguage
       return true;
     }
 
+    bool HasBodyTokens(Dafny.Declaration decl) {
+      Contract.Requires(decl != null);
+      return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;
+    }
+
     class ORegion
     {
       public readonly int Start;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
index 35e8f1f9..d822fbfc 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
@@ -16,5 +16,7 @@
   <References />
   <Content>
     <MefComponent>|%CurrentProject%|</MefComponent>
+    <CustomExtension Type="Boogie">DafnyPrelude.bpl</CustomExtension>
+    <CustomExtension Type="SMTLib 2">UnivBackPred2.smt2</CustomExtension>
   </Content>
 </Vsix>
-- 
cgit v1.2.3