DafnyExtension: Added menu for invoking specific Dafny functionality (e.g., compilation).

22 files changed, 1536 insertions, 11 deletions

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index d7063e8b..21220216 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -191,7 +191,7 @@ namespace Microsoft.Dafny
       return exitValue;

     }

 

-    private static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName)

+    public static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName)

     {

       Contract.Requires(dafnyProgram != null);

       // Compile the Dafny program into a string that contains the C# program

diff --git a/Source/DafnyExtension.sln b/Source/DafnyExtension.sln
index fd450cc8..83284c78 100644
--- a/Source/DafnyExtension.sln
+++ b/Source/DafnyExtension.sln
@@ -3,6 +3,8 @@ Microsoft Visual Studio Solution File, Format Version 12.00
 # Visual Studio 2012

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyExtension", "DafnyExtension\DafnyExtension.csproj", "{6E9A5E14-0763-471C-A129-80A879D9E7BA}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyMenu", "DafnyMenu\DafnyMenu.csproj", "{CA0848D3-3E4F-410E-8AC6-D6125A2B8E30}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Debug|Any CPU = Debug|Any CPU

@@ -13,6 +15,10 @@ Global
 		{6E9A5E14-0763-471C-A129-80A879D9E7BA}.Debug|Any CPU.Build.0 = Debug|Any CPU

 		{6E9A5E14-0763-471C-A129-80A879D9E7BA}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{6E9A5E14-0763-471C-A129-80A879D9E7BA}.Release|Any CPU.Build.0 = Release|Any CPU

+		{CA0848D3-3E4F-410E-8AC6-D6125A2B8E30}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{CA0848D3-3E4F-410E-8AC6-D6125A2B8E30}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{CA0848D3-3E4F-410E-8AC6-D6125A2B8E30}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{CA0848D3-3E4F-410E-8AC6-D6125A2B8E30}.Release|Any CPU.Build.0 = Release|Any CPU

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/DafnyExtension/ClassificationTagger.cs b/Source/DafnyExtension/ClassificationTagger.cs
index 09835ac9..8f6191e5 100644
--- a/Source/DafnyExtension/ClassificationTagger.cs
+++ b/Source/DafnyExtension/ClassificationTagger.cs
@@ -37,6 +37,8 @@ namespace DafnyLanguage
     ITagAggregator<DafnyTokenTag> _aggregator;

     IDictionary<DafnyTokenKinds, IClassificationType> _typeMap;

 

+    static bool DafnyMenuWasInitialized;

+

     internal DafnyClassifier(ITextBuffer buffer,

                              ITagAggregator<DafnyTokenTag> tagAggregator,

                              IClassificationTypeRegistryService typeService, Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService standards) {

@@ -51,6 +53,19 @@ namespace DafnyLanguage
       _typeMap[DafnyTokenKinds.Comment] = standards.Comment;

       _typeMap[DafnyTokenKinds.VariableIdentifier] = standards.Identifier;

       _typeMap[DafnyTokenKinds.VariableIdentifierDefinition] = typeService.GetClassificationType("Dafny identifier");

+

+      if (!DafnyMenuWasInitialized)

+      {

+        // Initialize the Dafny menu.

+        var shell = Microsoft.VisualStudio.Shell.Package.GetGlobalService(typeof(Microsoft.VisualStudio.Shell.Interop.SVsShell)) as Microsoft.VisualStudio.Shell.Interop.IVsShell;

+        if (shell != null)

+        {

+          Microsoft.VisualStudio.Shell.Interop.IVsPackage package = null;

+          Guid PackageToBeLoadedGuid = new Guid("e1baf989-88a6-4acf-8d97-e0dc243476aa");

+          shell.LoadPackage(ref PackageToBeLoadedGuid, out package);

+        }

+        DafnyMenuWasInitialized = true;

+      }

     }

 

     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index a2c60cca..27d17dfe 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -16,7 +16,7 @@ using VC;
 

 namespace DafnyLanguage

 {

-  class DafnyDriver

+  public class DafnyDriver

   {

     readonly string _programText;

     readonly string _filename;

@@ -120,6 +120,12 @@ namespace DafnyLanguage
       }

     }

 

+    public static void Compile(Dafny.Program dafnyProgram)

+    {

+      Microsoft.Dafny.DafnyOptions.O.SpillTargetCode = true;

+      Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(dafnyProgram, dafnyProgram.Name);

+    }

+

     enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }

 

     /// <summary>

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 3534366e..9399a1d2 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 ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

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

   <PropertyGroup>

@@ -88,9 +88,6 @@
       <SpecificVersion>False</SpecificVersion>

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

     </Reference>

-    <Reference Include="BVD">

-      <HintPath>..\..\..\boogie\Binaries\BVD.exe</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>

@@ -197,6 +194,9 @@
     <Content Include="UnivBackPred2.smt2">

       <IncludeInVSIX>true</IncludeInVSIX>

     </Content>

+    <Content Include="DafnyRuntime.cs">

+      <IncludeInVSIX>true</IncludeInVSIX>

+    </Content>

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

       <SubType>Designer</SubType>

     </None>

@@ -218,7 +218,8 @@
   </PropertyGroup>

   <PropertyGroup>

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

-copy /y $(SolutionDir)\..\Binaries\DafnyPrelude.bpl $(ProjectDir)</PreBuildEvent>

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

+copy /y $(SolutionDir)\..\Binaries\DafnyRuntime.cs $(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.

@@ -227,4 +228,4 @@ copy /y $(SolutionDir)\..\Binaries\DafnyPrelude.bpl $(ProjectDir)</PreBuildEvent
   <Target Name="AfterBuild">

   </Target>

   -->

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

diff --git a/Source/DafnyExtension/DafnyRuntime.cs b/Source/DafnyExtension/DafnyRuntime.cs
new file mode 100644
index 00000000..a8faafae
--- /dev/null
+++ b/Source/DafnyExtension/DafnyRuntime.cs
@@ -0,0 +1,631 @@
+using System.Numerics;

+

+namespace Dafny

+{

+  using System.Collections.Generic;

+

+  public class Set<T>

+  {

+    Dictionary<T, bool> dict;

+    Set(Dictionary<T, bool> d) {

+      dict = d;

+    }

+    public static Set<T> Empty {

+      get {

+        return new Set<T>(new Dictionary<T, bool>(0));

+      }

+    }

+    public static Set<T> FromElements(params T[] values) {

+      Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);

+      foreach (T t in values)

+        d[t] = true;

+      return new Set<T>(d);

+    }

+    public static Set<T> FromCollection(ICollection<T> values) {

+      Dictionary<T, bool> d = new Dictionary<T, bool>();

+      foreach (T t in values)

+        d[t] = true;

+      return new Set<T>(d);

+    }

+    

+    public IEnumerable<T> Elements {

+      get {

+        return dict.Keys;

+      }

+    }

+    /// <summary>

+    /// This is an inefficient iterator for producing all subsets of "this".  Each set returned is the same

+    /// Set<T> object (but this Set<T> object is fresh; in particular, it is not "this").

+    /// </summary>

+    public IEnumerable<Set<T>> AllSubsets {

+      get {

+        // Start by putting all set elements into a list

+        var elmts = new List<T>();

+        elmts.AddRange(dict.Keys);

+        var n = elmts.Count;

+        var which = new bool[n];

+        var s = new Set<T>(new Dictionary<T, bool>(0));

+        while (true) {

+          yield return s;

+          // "add 1" to "which", as if doing a carry chain.  For every digit changed, change the membership of the corresponding element in "s".

+          int i = 0;

+          for (; i < n && which[i]; i++) {

+            which[i] = false;

+            s.dict.Remove(elmts[i]);

+          }

+          if (i == n) {

+            // we have cycled through all the subsets

+            break;

+          }

+          which[i] = true;

+          s.dict.Add(elmts[i], true);

+        }

+      }

+    }

+    public bool Equals(Set<T> other) {

+      return dict.Count == other.dict.Count && IsSubsetOf(other);

+    }

+    public override bool Equals(object other) {

+      return other is Set<T> && Equals((Set<T>)other);

+    }

+    public override int GetHashCode() {

+      return dict.GetHashCode();

+    }

+    public override string ToString() {

+      var s = "{";

+      var sep = "";

+      foreach (var t in dict.Keys) {

+        s += sep + t.ToString();

+        sep = ", ";

+      }

+      return s + "}";

+    }

+    public bool IsProperSubsetOf(Set<T> other) {

+      return dict.Count < other.dict.Count && IsSubsetOf(other);

+    }

+    public bool IsSubsetOf(Set<T> other) {

+      if (other.dict.Count < dict.Count)

+        return false;

+      foreach (T t in dict.Keys) {

+        if (!other.dict.ContainsKey(t))

+          return false;

+      }

+      return true;

+    }

+    public bool IsSupersetOf(Set<T> other) {

+      return other.IsSubsetOf(this);

+    }

+    public bool IsProperSupersetOf(Set<T> other) {

+      return other.IsProperSubsetOf(this);

+    }

+    public bool IsDisjointFrom(Set<T> other) {

+      Dictionary<T, bool> a, b;

+      if (dict.Count < other.dict.Count) {

+        a = dict; b = other.dict;

+      } else {

+        a = other.dict; b = dict;

+      }

+      foreach (T t in a.Keys) {

+        if (b.ContainsKey(t))

+          return false;

+      }

+      return true;

+    }

+    public bool Contains(T t) {

+      return dict.ContainsKey(t);

+    }

+    public Set<T> Union(Set<T> other) {

+      if (dict.Count == 0)

+        return other;

+      else if (other.dict.Count == 0)

+        return this;

+      Dictionary<T, bool> a, b;

+      if (dict.Count < other.dict.Count) {

+        a = dict; b = other.dict;

+      } else {

+        a = other.dict; b = dict;

+      }

+      Dictionary<T, bool> r = new Dictionary<T, bool>();

+      foreach (T t in b.Keys)

+        r[t] = true;

+      foreach (T t in a.Keys)

+        r[t] = true;

+      return new Set<T>(r);

+    }

+    public Set<T> Intersect(Set<T> other) {

+      if (dict.Count == 0)

+        return this;

+      else if (other.dict.Count == 0)

+        return other;

+      Dictionary<T, bool> a, b;

+      if (dict.Count < other.dict.Count) {

+        a = dict; b = other.dict;

+      } else {

+        a = other.dict; b = dict;

+      }

+      var r = new Dictionary<T, bool>();

+      foreach (T t in a.Keys) {

+        if (b.ContainsKey(t))

+          r.Add(t, true);

+      }

+      return new Set<T>(r);

+    }

+    public Set<T> Difference(Set<T> other) {

+      if (dict.Count == 0)

+        return this;

+      else if (other.dict.Count == 0)

+        return this;

+      var r = new Dictionary<T, bool>();

+      foreach (T t in dict.Keys) {

+        if (!other.dict.ContainsKey(t))

+          r.Add(t, true);

+      }

+      return new Set<T>(r);

+    }

+  }

+  public class MultiSet<T>

+  {

+    Dictionary<T, int> dict;

+    MultiSet(Dictionary<T, int> d) {

+      dict = d;

+    }

+    public static MultiSet<T> Empty {

+      get {

+        return new MultiSet<T>(new Dictionary<T, int>(0));

+      }

+    }

+    public static MultiSet<T> FromElements(params T[] values) {

+      Dictionary<T, int> d = new Dictionary<T, int>(values.Length);

+      foreach (T t in values) {

+        var i = 0;

+        if (!d.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        d[t] = i + 1;

+      }

+      return new MultiSet<T>(d);

+    }

+    public static MultiSet<T> FromCollection(ICollection<T> values) {

+      Dictionary<T, int> d = new Dictionary<T, int>();

+      foreach (T t in values) {

+        var i = 0;

+        if (!d.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        d[t] = i + 1;

+      }

+      return new MultiSet<T>(d);

+    }

+    public static MultiSet<T> FromSeq(Sequence<T> values) {

+      Dictionary<T, int> d = new Dictionary<T, int>();

+      foreach (T t in values.Elements) {

+        var i = 0;

+        if (!d.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        d[t] = i + 1;

+      }

+      return new MultiSet<T>(d);

+    }

+    public static MultiSet<T> FromSet(Set<T> values) {

+      Dictionary<T, int> d = new Dictionary<T, int>();

+      foreach (T t in values.Elements) {

+        d[t] = 1;

+      }

+      return new MultiSet<T>(d);

+    }

+

+    public bool Equals(MultiSet<T> other) {

+      return other.IsSubsetOf(this) && this.IsSubsetOf(other);

+    }

+    public override bool Equals(object other) {

+      return other is MultiSet<T> && Equals((MultiSet<T>)other);

+    }

+    public override int GetHashCode() {

+      return dict.GetHashCode();

+    }

+    public override string ToString() {

+      var s = "multiset{";

+      var sep = "";

+      foreach (var kv in dict) {

+        var t = kv.Key.ToString();

+        for (int i = 0; i < kv.Value; i++) {

+          s += sep + t.ToString();

+          sep = ", ";

+        }

+      }

+      return s + "}";

+    }

+    public bool IsProperSubsetOf(MultiSet<T> other) {

+      return !Equals(other) && IsSubsetOf(other);

+    }

+    public bool IsSubsetOf(MultiSet<T> other) {

+      foreach (T t in dict.Keys) {

+        if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])

+          return false;

+      }

+      return true;

+    }

+    public bool IsSupersetOf(MultiSet<T> other) {

+      return other.IsSubsetOf(this);

+    }

+    public bool IsProperSupersetOf(MultiSet<T> other) {

+      return other.IsProperSubsetOf(this);

+    }

+    public bool IsDisjointFrom(MultiSet<T> other) {

+      foreach (T t in dict.Keys) {

+        if (other.dict.ContainsKey(t))

+          return false;

+      }

+      foreach (T t in other.dict.Keys) {

+        if (dict.ContainsKey(t))

+          return false;

+      }

+      return true;

+    }

+    public bool Contains(T t) {

+      return dict.ContainsKey(t);

+    }

+    public MultiSet<T> Union(MultiSet<T> other) {

+      if (dict.Count == 0)

+        return other;

+      else if (other.dict.Count == 0)

+        return this;

+      var r = new Dictionary<T, int>();

+      foreach (T t in dict.Keys) {

+        var i = 0;

+        if (!r.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        r[t] = i + dict[t];

+      }

+      foreach (T t in other.dict.Keys) {

+        var i = 0;

+        if (!r.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        r[t] = i + other.dict[t];

+      }

+      return new MultiSet<T>(r);

+    }

+    public MultiSet<T> Intersect(MultiSet<T> other) {

+      if (dict.Count == 0)

+        return this;

+      else if (other.dict.Count == 0)

+        return other;

+      var r = new Dictionary<T, int>();

+      foreach (T t in dict.Keys) {

+        if (other.dict.ContainsKey(t)) {

+          r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);

+        }

+      }

+      return new MultiSet<T>(r);

+    }

+    public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other

+      if (dict.Count == 0)

+        return this;

+      else if (other.dict.Count == 0)

+        return this;

+      var r = new Dictionary<T, int>();

+      foreach (T t in dict.Keys) {

+        if (!other.dict.ContainsKey(t)) {

+          r.Add(t, dict[t]);

+        } else if (other.dict[t] < dict[t]) {

+          r.Add(t, dict[t] - other.dict[t]);

+        }

+      }

+      return new MultiSet<T>(r);

+    }

+    public IEnumerable<T> Elements {

+      get {

+        List<T> l = new List<T>();

+        foreach (T t in dict.Keys) {

+          int n;

+          dict.TryGetValue(t, out n);

+          for (int i = 0; i < n; i ++) {

+            l.Add(t);

+          }

+        }

+        return l;

+      }

+    }

+  }

+

+  public class Map<U, V>

+  {

+    Dictionary<U, V> dict;

+    Map(Dictionary<U, V> d) {

+      dict = d;

+    }

+    public static Map<U, V> Empty {

+      get {

+        return new Map<U, V>(new Dictionary<U,V>());

+      }

+    }

+    public static Map<U, V> FromElements(params Pair<U, V>[] values) {

+      Dictionary<U, V> d = new Dictionary<U, V>(values.Length);

+      foreach (Pair<U, V> p in values) {

+        d[p.Car] = p.Cdr;

+      }

+      return new Map<U, V>(d);

+    }

+    public static Map<U, V> FromCollection(List<Pair<U, V>> values) {

+      Dictionary<U, V> d = new Dictionary<U, V>(values.Count);

+      foreach (Pair<U, V> p in values) {

+        d[p.Car] = p.Cdr;

+      }

+      return new Map<U, V>(d);

+    }

+    public bool Equals(Map<U, V> other) {

+      foreach (U u in dict.Keys) {

+        V v1, v2;

+        if (!dict.TryGetValue(u, out v1)) {

+          return false; // this shouldn't happen

+        }

+        if (!other.dict.TryGetValue(u, out v2)) {

+          return false; // other dictionary does not contain this element

+        }

+        if (!v1.Equals(v2)) {

+          return false;

+        }

+      }

+      foreach (U u in other.dict.Keys) {

+        if (!dict.ContainsKey(u)) {

+          return false; // this shouldn't happen

+        }

+      }

+      return true;

+    }

+    public override bool Equals(object other) {

+      return other is Map<U, V> && Equals((Map<U, V>)other);

+    }

+    public override int GetHashCode() {

+      return dict.GetHashCode();

+    }

+    public override string ToString() {

+      var s = "map[";

+      var sep = "";

+      foreach (var kv in dict) {

+        s += sep + kv.Key.ToString() + " := " + kv.Value.ToString();

+        sep = ", ";

+      }

+      return s + "]";

+    }

+    public bool IsDisjointFrom(Map<U, V> other) {

+      foreach (U u in dict.Keys) {

+        if (other.dict.ContainsKey(u))

+          return false;

+      }

+      foreach (U u in other.dict.Keys) {

+        if (dict.ContainsKey(u))

+          return false;

+      }

+      return true;

+    }

+    public bool Contains(U u) {

+      return dict.ContainsKey(u);

+    }

+    public V Select(U index) {

+      return dict[index];

+    }

+    public Map<U, V> Update(U index, V val) {

+      Dictionary<U, V> d = new Dictionary<U, V>(dict);

+      d[index] = val;

+      return new Map<U, V>(d);

+    }

+    public IEnumerable<U> Domain {

+      get {

+        return dict.Keys;

+      }

+    }

+  }

+  public class Sequence<T>

+  {

+    T[] elmts;

+    public Sequence(T[] ee) {

+      elmts = ee;

+    }

+    public static Sequence<T> Empty {

+      get {

+        return new Sequence<T>(new T[0]);

+      }

+    }

+    public static Sequence<T> FromElements(params T[] values) {

+      return new Sequence<T>(values);

+    }

+    public BigInteger Length {

+      get { return new BigInteger(elmts.Length); }

+    }

+    public T[] Elements {

+      get {

+        return elmts;

+      }

+    }

+    public IEnumerable<T> UniqueElements {

+      get {

+        var st = Set<T>.FromElements(elmts);

+        return st.Elements;

+      }

+    }

+    public T Select(BigInteger index) {

+      return elmts[(int)index];

+    }

+    public Sequence<T> Update(BigInteger index, T t) {

+      T[] a = (T[])elmts.Clone();

+      a[(int)index] = t;

+      return new Sequence<T>(a);

+    }

+    public bool Equals(Sequence<T> other) {

+      int n = elmts.Length;

+      return n == other.elmts.Length && EqualUntil(other, n);

+    }

+    public override bool Equals(object other) {

+      return other is Sequence<T> && Equals((Sequence<T>)other);

+    }

+    public override int GetHashCode() {

+      return elmts.GetHashCode();

+    }

+    public override string ToString() {

+      var s = "[";

+      var sep = "";

+      foreach (var t in elmts) {

+        s += sep + t.ToString();

+        sep = ", ";

+      }

+      return s + "]";

+    }

+    bool EqualUntil(Sequence<T> other, int n) {

+      for (int i = 0; i < n; i++) {

+        if (!elmts[i].Equals(other.elmts[i]))

+          return false;

+      }

+      return true;

+    }

+    public bool IsProperPrefixOf(Sequence<T> other) {

+      int n = elmts.Length;

+      return n < other.elmts.Length && EqualUntil(other, n);

+    }

+    public bool IsPrefixOf(Sequence<T> other) {

+      int n = elmts.Length;

+      return n <= other.elmts.Length && EqualUntil(other, n);

+    }

+    public Sequence<T> Concat(Sequence<T> other) {

+      if (elmts.Length == 0)

+        return other;

+      else if (other.elmts.Length == 0)

+        return this;

+      T[] a = new T[elmts.Length + other.elmts.Length];

+      System.Array.Copy(elmts, 0, a, 0, elmts.Length);

+      System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);

+      return new Sequence<T>(a);

+    }

+    public bool Contains(T t) {

+      int n = elmts.Length;

+      for (int i = 0; i < n; i++) {

+        if (t.Equals(elmts[i]))

+          return true;

+      }

+      return false;

+    }

+    public Sequence<T> Take(BigInteger n) {

+      int m = (int)n;

+      if (elmts.Length == m)

+        return this;

+      T[] a = new T[m];

+      System.Array.Copy(elmts, a, m);

+      return new Sequence<T>(a);

+    }

+    public Sequence<T> Drop(BigInteger n) {

+      if (n.IsZero)

+        return this;

+      int m = (int)n;

+      T[] a = new T[elmts.Length - m];

+      System.Array.Copy(elmts, m, a, 0, elmts.Length - m);

+      return new Sequence<T>(a);

+    }

+  }

+  public struct Pair<A, B>

+  {

+    public readonly A Car;

+    public readonly B Cdr;

+    public Pair(A a, B b) {

+      this.Car = a;

+      this.Cdr = b;

+    }

+  }

+  public partial class Helpers {

+    // Computing forall/exists quantifiers

+    public static bool QuantBool(bool frall, System.Predicate<bool> pred) {

+      if (frall) {

+        return pred(false) && pred(true);

+      } else {

+        return pred(false) || pred(true);

+      }

+    }

+    public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {

+      for (BigInteger i = lo; i < hi; i++) {

+        if (pred(i) != frall) { return !frall; }

+      }

+      return frall;

+    }

+    public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {

+      foreach (var u in set.Elements) {

+        if (pred(u) != frall) { return !frall; }

+      }

+      return frall;

+    }

+    public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {

+      foreach (var u in map.Domain) {

+        if (pred(u) != frall) { return !frall; }

+      }

+      return frall;

+    }

+    public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {

+      foreach (var u in seq.Elements) {

+        if (pred(u) != frall) { return !frall; }

+      }

+      return frall;

+    }

+    public static bool QuantDatatype<U>(IEnumerable<U> set, bool frall, System.Predicate<U> pred) {

+      foreach (var u in set) {

+        if (pred(u) != frall) { return !frall; }

+      }

+      return frall;

+    }

+    // Enumerating other collections

+    public delegate Dafny.Set<T> ComprehensionDelegate<T>();

+    public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();

+    public static IEnumerable<bool> AllBooleans {

+      get {

+        yield return false;

+        yield return true;

+      }

+    }

+    // pre: b != 0

+    // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)

+    public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {

+      if (0 <= a.Sign) {

+        if (0 <= b.Sign) {

+          // +a +b: a/b

+          return BigInteger.Divide(a, b);

+        } else {

+          // +a -b: -(a/(-b))

+          return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));

+        }

+      } else {

+        if (0 <= b.Sign) {

+          // -a +b: -((-a-1)/b) - 1

+          return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;

+        } else {

+          // -a -b: ((-a-1)/(-b)) + 1

+          return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;

+        }

+      }

+    }

+    // pre: b != 0

+    // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)

+    public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {

+      var bp = BigInteger.Abs(b);

+      if (0 <= a.Sign) {

+        // +a: a % b'

+        return BigInteger.Remainder(a, bp);

+      } else {

+        // c = ((-a) % b')

+        // -a: b' - c if c > 0

+        // -a: 0 if c == 0

+        var c = BigInteger.Remainder(BigInteger.Negate(a), bp);

+        return c.IsZero ? c : BigInteger.Subtract(bp, c);

+      }

+    }

+    public static Sequence<T> SeqFromArray<T>(T[] array) {

+      return new Sequence<T>(array);

+    }

+    // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the

+    // method if possible.  Method "ExpressionSequence" would be a good candidate for it:

+    // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]

+    public static U ExpressionSequence<T, U>(T t, U u)

+    {

+      return u;

+    }

+  }

+}

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 7fdf38a6..3f4da8ed 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -79,7 +79,7 @@ namespace DafnyLanguage
     }

   }

 

-  internal class ProgressTagger : ITagger<ProgressGlyphTag>

+  internal class ProgressTagger : ITagger<ProgressGlyphTag>, IDisposable

   {

     ErrorListProvider _errorProvider;

     ITextBuffer _buffer;

@@ -100,6 +100,7 @@ namespace DafnyLanguage
     }

 

     public void Dispose() {

+      _errorProvider.Dispose();

     }

 

     // The following fields and the contents of the following two lists are protected by the lock "this".

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index ca9ed169..81efe28a 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -6,6 +6,7 @@
 using EnvDTE;

 using System;

 using System.Collections.Generic;

+using System.Collections.Concurrent;

 using System.Linq;

 using System.Text;

 using System.ComponentModel.Composition;

@@ -66,7 +67,7 @@ namespace DafnyLanguage
   /// <summary>

   /// Translate PkgDefTokenTags into ErrorTags and Error List items

   /// </summary>

-  internal sealed class ResolverTagger : ITagger<DafnyResolverTag>, IDisposable

+  public sealed class ResolverTagger : ITagger<DafnyResolverTag>, IDisposable

   {

     ITextBuffer _buffer;

     ITextDocument _document;

@@ -77,6 +78,8 @@ namespace DafnyLanguage
     List<DafnyError> _verificationErrors = new List<DafnyError>();

     ErrorListProvider _errorProvider;

 

+    public static IDictionary<string, Dafny.Program> Programs = new ConcurrentDictionary<string, Dafny.Program>();

+

     internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) {

       _buffer = buffer;

       if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document))

@@ -178,6 +181,16 @@ namespace DafnyLanguage
         _snapshot = snapshot;

         _program = program;

       }

+

+      if (program != null && _document != null)

+      {

+        Programs[_document.FilePath] = program;

+      }

+      else if (_document != null)

+      {

+        Programs.Remove(_document.FilePath);

+      }

+

       PopulateErrorList(newErrors, false, snapshot);

     }

 

@@ -287,7 +300,7 @@ namespace DafnyLanguage
     ProcessError, ParseWarning, ParseError, ResolveError, VerificationError, AuxInformation, InternalError

   }

 

-  internal class DafnyError

+  public class DafnyError

   {

     public readonly int Line;  // 0 based

     public readonly int Column;  // 0 based

diff --git a/Source/DafnyExtension/source.extension.vsixmanifest b/Source/DafnyExtension/source.extension.vsixmanifest
index ef5c1cf5..e3e2623f 100644
--- a/Source/DafnyExtension/source.extension.vsixmanifest
+++ b/Source/DafnyExtension/source.extension.vsixmanifest
@@ -19,6 +19,7 @@
   <References />

   <Content>

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

+    <VsPackage>DafnyMenu</VsPackage>

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

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

   </Content>

diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
new file mode 100644
index 00000000..3df7f083
--- /dev/null
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -0,0 +1,181 @@
+<?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>

+    <VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">11.0</VisualStudioVersion>

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

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

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{CA0848D3-3E4F-410E-8AC6-D6125A2B8E30}</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.DafnyMenu</RootNamespace>

+    <AssemblyName>DafnyMenu</AssemblyName>

+    <SignAssembly>false</SignAssembly>

+    <AssemblyOriginatorKeyFile>

+    </AssemblyOriginatorKeyFile>

+    <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

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

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+    <RunCodeAnalysis>true</RunCodeAnalysis>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="DafnyPipeline">

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

+    </Reference>

+    <Reference Include="Microsoft.CSharp" />

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

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

+    <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.Shell.Interop.11.0">

+      <EmbedInteropTypes>true</EmbedInteropTypes>

+    </Reference>

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

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

+    <Reference Include="Microsoft.VisualStudio.Shell.11.0" />

+    <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0" />

+    <Reference Include="Microsoft.VisualStudio.Shell.Immutable.11.0" />

+    <Reference Include="System" />

+    <Reference Include="System.Core" />

+    <Reference Include="System.Data" />

+    <Reference Include="System.Design" />

+    <Reference Include="System.Drawing" />

+    <Reference Include="System.Windows.Forms" />

+    <Reference Include="System.Xml" />

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

+    <COMReference Include="EnvDTE100">

+      <Guid>{26AD1324-4B7C-44BC-84F8-B86AED45729F}</Guid>

+      <VersionMajor>10</VersionMajor>

+      <VersionMinor>0</VersionMinor>

+      <Lcid>0</Lcid>

+      <WrapperTool>primary</WrapperTool>

+      <Isolated>False</Isolated>

+      <EmbedInteropTypes>False</EmbedInteropTypes>

+    </COMReference>

+    <COMReference Include="EnvDTE80">

+      <Guid>{1A31287A-4D7D-413E-8E32-3B374931BD89}</Guid>

+      <VersionMajor>8</VersionMajor>

+      <VersionMinor>0</VersionMinor>

+      <Lcid>0</Lcid>

+      <WrapperTool>primary</WrapperTool>

+      <Isolated>False</Isolated>

+      <EmbedInteropTypes>False</EmbedInteropTypes>

+    </COMReference>

+    <COMReference Include="EnvDTE90">

+      <Guid>{2CE2370E-D744-4936-A090-3FFFE667B0E1}</Guid>

+      <VersionMajor>9</VersionMajor>

+      <VersionMinor>0</VersionMinor>

+      <Lcid>0</Lcid>

+      <WrapperTool>primary</WrapperTool>

+      <Isolated>False</Isolated>

+      <EmbedInteropTypes>False</EmbedInteropTypes>

+    </COMReference>

+    <COMReference Include="Microsoft.VisualStudio.CommandBars">

+      <Guid>{1CBA492E-7263-47BB-87FE-639000619B15}</Guid>

+      <VersionMajor>8</VersionMajor>

+      <VersionMinor>0</VersionMinor>

+      <Lcid>0</Lcid>

+      <WrapperTool>primary</WrapperTool>

+      <Isolated>False</Isolated>

+      <EmbedInteropTypes>False</EmbedInteropTypes>

+    </COMReference>

+    <COMReference Include="stdole">

+      <Guid>{00020430-0000-0000-C000-000000000046}</Guid>

+      <VersionMajor>2</VersionMajor>

+      <VersionMinor>0</VersionMinor>

+      <Lcid>0</Lcid>

+      <WrapperTool>primary</WrapperTool>

+      <Isolated>False</Isolated>

+      <EmbedInteropTypes>False</EmbedInteropTypes>

+    </COMReference>

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="Guids.cs" />

+    <Compile Include="Resources.Designer.cs">

+      <AutoGen>True</AutoGen>

+      <DesignTime>True</DesignTime>

+      <DependentUpon>Resources.resx</DependentUpon>

+    </Compile>

+    <Compile Include="GlobalSuppressions.cs" />

+    <Compile Include="DafnyMenuPackage.cs" />

+    <Compile Include="Properties\AssemblyInfo.cs" />

+    <Compile Include="PkgCmdID.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <EmbeddedResource Include="Resources.resx">

+      <Generator>ResXFileCodeGenerator</Generator>

+      <LastGenOutput>Resources.Designer.cs</LastGenOutput>

+      <SubType>Designer</SubType>

+    </EmbeddedResource>

+    <EmbeddedResource Include="VSPackage.resx">

+      <MergeWithCTO>true</MergeWithCTO>

+      <ManifestResourceName>VSPackage</ManifestResourceName>

+    </EmbeddedResource>

+  </ItemGroup>

+  <ItemGroup>

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

+      <SubType>Designer</SubType>

+    </None>

+  </ItemGroup>

+  <ItemGroup>

+    <VSCTCompile Include="DafnyMenu.vsct">

+      <ResourceName>Menus.ctmenu</ResourceName>

+    </VSCTCompile>

+  </ItemGroup>

+  <ItemGroup>

+    <None Include="Resources\Images.png" />

+  </ItemGroup>

+  <ItemGroup>

+    <Content Include="Resources\Package.ico" />

+  </ItemGroup>

+  <ItemGroup>

+    <ProjectReference Include="..\DafnyExtension\DafnyExtension.csproj">

+      <Project>{6e9a5e14-0763-471c-a129-80a879d9e7ba}</Project>

+      <Name>DafnyExtension</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <PropertyGroup>

+    <UseCodebase>true</UseCodebase>

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

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>
\ No newline at end of file
diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
new file mode 100644
index 00000000..1d0c783b
--- /dev/null
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -0,0 +1,121 @@
+<?xml version="1.0" encoding="utf-8"?>

+<CommandTable xmlns="http://schemas.microsoft.com/VisualStudio/2005-10-18/CommandTable" xmlns:xs="http://www.w3.org/2001/XMLSchema">

+

+  <!--  This is the file that defines the actual layout and type of the commands.

+        It is divided in different sections (e.g. command definition, command

+        placement, ...), with each defining a specific set of properties.

+        See the comment before each section for more details about how to

+        use it. -->

+

+  <!--  The VSCT compiler (the tool that translates this file into the binary 

+        format that VisualStudio will consume) has the ability to run a preprocessor 

+        on the vsct file; this preprocessor is (usually) the C++ preprocessor, so 

+        it is possible to define includes and macros with the same syntax used 

+        in C++ files. Using this ability of the compiler here, we include some files 

+        defining some of the constants that we will use inside the file. -->

+

+  <!--This is the file that defines the IDs for all the commands exposed by VisualStudio. -->

+  <Extern href="stdidcmd.h"/>

+

+  <!--This header contains the command ids for the menus provided by the shell. -->

+  <Extern href="vsshlids.h"/>

+

+  <!--The Commands section is where we the commands, menus and menu groups are defined.

+      This section uses a Guid to identify the package that provides the command defined inside it. -->

+  <Commands package="guidDafnyMenuPkg">

+    <!-- Inside this section we have different sub-sections: one for the menus, another  

+    for the menu groups, one for the buttons (the actual commands), one for the combos 

+    and the last one for the bitmaps used. Each element is identified by a command id that  

+    is a unique pair of guid and numeric identifier; the guid part of the identifier is usually  

+    called "command set" and is used to group different command inside a logically related  

+    group; your package should define its own command set in order to avoid collisions  

+    with command ids defined by other packages. -->

+

+

+    <!-- In this section you can define new menu groups. A menu group is a container for 

+         other menus or buttons (commands); from a visual point of view you can see the 

+         group as the part of a menu contained between two lines. The parent of a group 

+         must be a menu. -->

+

+    <Menus>

+      <Menu guid="guidDafnyMenuPkg" id="DafnyMenu" priority="0x700" type="Menu">

+        <CommandFlag>DefaultInvisible</CommandFlag>

+        <CommandFlag>DynamicVisibility</CommandFlag>

+        <Parent guid="guidSHLMainMenu" id="IDG_VS_MM_TOOLSADDINS" />

+        <Strings>

+          <CommandName>Dafny</CommandName>

+        </Strings>

+      </Menu>

+    </Menus>

+

+    <Groups>

+      <Group guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" priority="0x0600">

+        <Parent guid="guidDafnyMenuPkg" id="DafnyMenu"/>

+      </Group>

+    </Groups>

+

+    <!--Buttons section. -->

+    <!--This section defines the elements the user can interact with, like a menu command or a button 

+        or combo box in a toolbar. -->

+    <Buttons>

+

+      <!--To define a menu group you have to specify its ID, the parent menu and its display priority. 

+          The command is visible and enabled by default. If you need to change the visibility, status, etc, you can use

+          the CommandFlag node.

+          You can add more than one CommandFlag node e.g.:

+              <CommandFlag>DefaultInvisible</CommandFlag>

+              <CommandFlag>DynamicVisibility</CommandFlag>

+          If you do not want an image next to your command, remove the Icon node /> -->

+

+      <Button guid="guidDafnyMenuCmdSet" id="cmdidCompile" priority="0x0100" type="Button">

+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />

+        <!--

+        <Icon guid="guidImages" id="bmpPic1" />

+        -->

+        <Strings>

+          <ButtonText>Compile</ButtonText>

+        </Strings>

+      </Button>

+

+    </Buttons>

+

+    <!--The bitmaps section is used to define the bitmaps that are used for the commands.-->

+    <Bitmaps>

+      <!--  The bitmap id is defined in a way that is a little bit different from the others: 

+            the declaration starts with a guid for the bitmap strip, then there is the resource id of the 

+            bitmap strip containing the bitmaps and then there are the numeric ids of the elements used 

+            inside a button definition. An important aspect of this declaration is that the element id 

+            must be the actual index (1-based) of the bitmap inside the bitmap strip. -->

+

+      <!--

+      <Bitmap guid="guidImages" href="Resources\Images.png" usedList="bmpPic1, bmpPic2, bmpPicSearch, bmpPicX, bmpPicArrows"/>

+      -->

+    </Bitmaps>

+

+  </Commands>

+

+  <Symbols>

+    <!-- This is the package guid. -->

+    <GuidSymbol name="guidDafnyMenuPkg" value="{e1baf989-88a6-4acf-8d97-e0dc243476aa}">

+      <IDSymbol name="DafnyMenu" value="0x1021" />

+    </GuidSymbol>

+

+    <!-- This is the guid used to group the menu commands together -->

+    <GuidSymbol name="guidDafnyMenuCmdSet" value="{393ad46d-e125-41ce-84ee-b4d552d5ba16}">

+      <IDSymbol name="DafnyMenuGroup" value="0x1020" />

+      <IDSymbol name="cmdidCompile" value="0x0100" />

+    </GuidSymbol>

+

+    <!--

+    <GuidSymbol name="guidImages" value="{0176b216-66c6-49f6-a97d-0273c57a7da6}" >

+      <IDSymbol name="bmpPic1" value="1" />

+      <IDSymbol name="bmpPic2" value="2" />

+      <IDSymbol name="bmpPicSearch" value="3" />

+      <IDSymbol name="bmpPicX" value="4" />

+      <IDSymbol name="bmpPicArrows" value="5" />

+      <IDSymbol name="bmpPicStrikethrough" value="6" />

+    </GuidSymbol>

+    -->

+  </Symbols>

+

+</CommandTable>

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
new file mode 100644
index 00000000..c0784955
--- /dev/null
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -0,0 +1,126 @@
+using System;

+using System.Diagnostics;

+using System.Globalization;

+using System.Runtime.InteropServices;

+using System.ComponentModel.Design;

+using Microsoft.Win32;

+using Microsoft.VisualStudio;

+using Microsoft.VisualStudio.Shell.Interop;

+using Microsoft.VisualStudio.OLE.Interop;

+using Microsoft.VisualStudio.Shell;

+

+namespace DafnyLanguage.DafnyMenu

+{

+  /// <summary>

+  /// This is the class that implements the package exposed by this assembly.

+  ///

+  /// The minimum requirement for a class to be considered a valid package for Visual Studio

+  /// is to implement the IVsPackage interface and register itself with the shell.

+  /// This package uses the helper classes defined inside the Managed Package Framework (MPF)

+  /// to do it: it derives from the Package class that provides the implementation of the 

+  /// IVsPackage interface and uses the registration attributes defined in the framework to 

+  /// register itself and its components with the shell.

+  /// </summary>

+  // This attribute tells the PkgDef creation utility (CreatePkgDef.exe) that this class is

+  // a package.

+  [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", IconResourceID = 400)]

+  // 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}")]

+  [Guid(GuidList.guidDafnyMenuPkgString)]

+  public sealed class DafnyMenuPackage : Package

+  {

+

+    private OleMenuCommand compileCommand;

+    private OleMenuCommand menuCommand;

+

+    /// <summary>

+    /// Default constructor of the package.

+    /// Inside this method you can place any initialization code that does not require 

+    /// any Visual Studio service because at this point the package object is created but 

+    /// not sited yet inside Visual Studio environment. The place to do all the other 

+    /// initialization is the Initialize method.

+    /// </summary>

+    public DafnyMenuPackage()

+    {

+      Debug.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString()));

+    }

+

+

+    #region Package Members

+

+    /// <summary>

+    /// Initialization of the package; this method is called right after the package is sited, so this is the place

+    /// where you can put all the initialization code that rely on services provided by VisualStudio.

+    /// </summary>

+    protected override void Initialize()

+    {

+      Debug.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering Initialize() of: {0}", this.ToString()));

+      base.Initialize();

+

+      // Add our command handlers for menu (commands must exist in the .vsct file)

+      var mcs = GetService(typeof(IMenuCommandService)) as OleMenuCommandService;

+      if (null != mcs)

+      {

+        // Create the command for the menu item.

+        var compileCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidCompile);

+        compileCommand = new OleMenuCommand(CompileCallback, compileCommandID);

+        compileCommand.Enabled = false;

+        compileCommand.BeforeQueryStatus += compileCommand_BeforeQueryStatus;

+        mcs.AddCommand(compileCommand);

+

+        var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);

+        menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);

+        menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;

+        menuCommand.Enabled = true;

+        var s = menuCommand.OleStatus;

+        mcs.AddCommand(menuCommand);

+      }

+    }

+

+    void menuCommand_BeforeQueryStatus(object sender, EventArgs e)

+    {

+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

+      var isActive = dte.ActiveDocument.FullName.EndsWith(".dfy");

+      menuCommand.Visible = isActive;

+      menuCommand.Enabled = isActive;

+    }

+

+    void compileCommand_BeforeQueryStatus(object sender, EventArgs e)

+    {

+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

+      Microsoft.Dafny.Program program;

+      DafnyLanguage.ResolverTagger.Programs.TryGetValue(dte.ActiveDocument.FullName, out program);

+      compileCommand.Enabled = (program != null);

+    }

+

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

+    {

+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

+      Microsoft.Dafny.Program program;

+      DafnyLanguage.ResolverTagger.Programs.TryGetValue(dte.ActiveDocument.FullName, out program);

+

+      if (program != null)

+      {

+        IVsStatusbar statusBar = (IVsStatusbar)GetGlobalService(typeof(SVsStatusbar));

+        uint cookie = 0;

+        statusBar.Progress(ref cookie, 1, "Compiling...", 0, 0);

+

+        DafnyDriver.Compile(program);

+

+        statusBar.Progress(ref cookie, 0, "", 0, 0);

+      }

+    }

+  }

+}

diff --git a/Source/DafnyMenu/GlobalSuppressions.cs b/Source/DafnyMenu/GlobalSuppressions.cs
new file mode 100644
index 00000000..3689ed23
--- /dev/null
+++ b/Source/DafnyMenu/GlobalSuppressions.cs
@@ -0,0 +1 @@
+[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1017:MarkAssembliesWithComVisible")]

diff --git a/Source/DafnyMenu/Guids.cs b/Source/DafnyMenu/Guids.cs
new file mode 100644
index 00000000..dc392c09
--- /dev/null
+++ b/Source/DafnyMenu/Guids.cs
@@ -0,0 +1,15 @@
+// Guids.cs

+// MUST match guids.h

+using System;

+

+namespace DafnyLanguage.DafnyMenu

+{

+  static class GuidList

+  {

+    public const string guidDafnyMenuPkgString = "e1baf989-88a6-4acf-8d97-e0dc243476aa";

+    public const string guidDafnyMenuCmdSetString = "393ad46d-e125-41ce-84ee-b4d552d5ba16";

+

+    public static readonly Guid guidDafnyMenuCmdSet = new Guid(guidDafnyMenuCmdSetString);

+    public static readonly Guid guidDafnyMenuPkgSet = new Guid(guidDafnyMenuPkgString);

+  };

+}
\ No newline at end of file
diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
new file mode 100644
index 00000000..1b786829
--- /dev/null
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -0,0 +1,12 @@
+// PkgCmdID.cs

+// MUST match PkgCmdID.h

+using System;

+

+namespace DafnyLanguage.DafnyMenu

+{

+  static class PkgCmdIDList

+  {

+    public const uint cmdidCompile = 0x100;

+    public const uint cmdidMenu = 0x1021;

+  };

+}
\ No newline at end of file
diff --git a/Source/DafnyMenu/Properties/AssemblyInfo.cs b/Source/DafnyMenu/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..91380a74
--- /dev/null
+++ b/Source/DafnyMenu/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+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 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("DafnyMenu")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

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

+[assembly: AssemblyProduct("DafnyMenu")]

+[assembly: AssemblyCopyright("")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]   

+[assembly: ComVisible(false)]     

+[assembly: CLSCompliant(false)]

+[assembly: NeutralResourcesLanguage("en-US")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Revision and Build Numbers 

+// by using the '*' as shown below:

+

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]

+

+

+

diff --git a/Source/DafnyMenu/Resources.Designer.cs b/Source/DafnyMenu/Resources.Designer.cs
new file mode 100644
index 00000000..f9fefb73
--- /dev/null
+++ b/Source/DafnyMenu/Resources.Designer.cs
@@ -0,0 +1,72 @@
+//------------------------------------------------------------------------------

+// <auto-generated>

+//     This code was generated by a tool.

+//     Runtime Version:4.0.30319.18033

+//

+//     Changes to this file may cause incorrect behavior and will be lost if

+//     the code is regenerated.

+// </auto-generated>

+//------------------------------------------------------------------------------

+

+namespace DafnyLanguage.DafnyMenu

+{

+  using System;

+

+

+  /// <summary>

+  ///   A strongly-typed resource class, for looking up localized strings, etc.

+  /// </summary>

+  // This class was auto-generated by the StronglyTypedResourceBuilder

+  // class via a tool like ResGen or Visual Studio.

+  // To add or remove a member, edit your .ResX file then rerun ResGen

+  // with the /str option, or rebuild your VS project.

+  [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")]

+  [global::System.Diagnostics.DebuggerNonUserCodeAttribute()]

+  [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()]

+  internal class Resources

+  {

+

+    private static global::System.Resources.ResourceManager resourceMan;

+

+    private static global::System.Globalization.CultureInfo resourceCulture;

+

+    [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")]

+    internal Resources()

+    {

+    }

+

+    /// <summary>

+    ///   Returns the cached ResourceManager instance used by this class.

+    /// </summary>

+    [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]

+    internal static global::System.Resources.ResourceManager ResourceManager

+    {

+      get

+      {

+        if (object.ReferenceEquals(resourceMan, null))

+        {

+          global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("DafnyLanguage.DafnyMenu.Resources", typeof(Resources).Assembly);

+          resourceMan = temp;

+        }

+        return resourceMan;

+      }

+    }

+

+    /// <summary>

+    ///   Overrides the current thread's CurrentUICulture property for all

+    ///   resource lookups using this strongly typed resource class.

+    /// </summary>

+    [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]

+    internal static global::System.Globalization.CultureInfo Culture

+    {

+      get

+      {

+        return resourceCulture;

+      }

+      set

+      {

+        resourceCulture = value;

+      }

+    }

+  }

+}

diff --git a/Source/DafnyMenu/Resources.resx b/Source/DafnyMenu/Resources.resx
new file mode 100644
index 00000000..352987aa
--- /dev/null
+++ b/Source/DafnyMenu/Resources.resx
@@ -0,0 +1,129 @@
+<?xml version="1.0" encoding="utf-8"?>

+<!--

+    VS SDK Notes: This resx file contains the resources that will be consumed directly by your package.

+    For example, if you chose to create a tool window, there is a resource with ID 'CanNotCreateWindow'. This

+    is used in VsPkg.cs to determine the string to show the user if there is an error when attempting to create

+    the tool window.

+

+    Resources that are accessed directly from your package *by Visual Studio* are stored in the VSPackage.resx 

+    file.

+-->

+<root>

+  <!-- 

+    Microsoft ResX Schema 

+    

+    Version 2.0

+    

+    The primary goals of this format is to allow a simple XML format 

+    that is mostly human readable. The generation and parsing of the 

+    various data types are done through the TypeConverter classes 

+    associated with the data types.

+    

+    Example:

+    

+    ... ado.net/XML headers & schema ...

+    <resheader name="resmimetype">text/microsoft-resx</resheader>

+    <resheader name="version">2.0</resheader>

+    <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader>

+    <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader>

+    <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data>

+    <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data>

+    <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64">

+        <value>[base64 mime encoded serialized .NET Framework object]</value>

+    </data>

+    <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">

+        <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value>

+        <comment>This is a comment</comment>

+    </data>

+                

+    There are any number of "resheader" rows that contain simple 

+    name/value pairs.

+    

+    Each data row contains a name, and value. The row also contains a 

+    type or mimetype. Type corresponds to a .NET class that support 

+    text/value conversion through the TypeConverter architecture. 

+    Classes that don't support this are serialized and stored with the 

+    mimetype set.

+    

+    The mimetype is used for serialized objects, and tells the 

+    ResXResourceReader how to depersist the object. This is currently not 

+    extensible. For a given mimetype the value must be set accordingly:

+    

+    Note - application/x-microsoft.net.object.binary.base64 is the format 

+    that the ResXResourceWriter will generate, however the reader can 

+    read any of the formats listed below.

+    

+    mimetype: application/x-microsoft.net.object.binary.base64

+    value   : The object must be serialized with 

+            : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter

+            : and then encoded with base64 encoding.

+    

+    mimetype: application/x-microsoft.net.object.soap.base64

+    value   : The object must be serialized with 

+            : System.Runtime.Serialization.Formatters.Soap.SoapFormatter

+            : and then encoded with base64 encoding.

+

+    mimetype: application/x-microsoft.net.object.bytearray.base64

+    value   : The object must be serialized into a byte array 

+            : using a System.ComponentModel.TypeConverter

+            : and then encoded with base64 encoding.

+    -->

+  <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata">

+    <xsd:import namespace="http://www.w3.org/XML/1998/namespace" />

+    <xsd:element name="root" msdata:IsDataSet="true">

+      <xsd:complexType>

+        <xsd:choice maxOccurs="unbounded">

+          <xsd:element name="metadata">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" />

+              </xsd:sequence>

+              <xsd:attribute name="name" use="required" type="xsd:string" />

+              <xsd:attribute name="type" type="xsd:string" />

+              <xsd:attribute name="mimetype" type="xsd:string" />

+              <xsd:attribute ref="xml:space" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="assembly">

+            <xsd:complexType>

+              <xsd:attribute name="alias" type="xsd:string" />

+              <xsd:attribute name="name" type="xsd:string" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="data">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+                <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" />

+              <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" />

+              <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" />

+              <xsd:attribute ref="xml:space" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="resheader">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" use="required" />

+            </xsd:complexType>

+          </xsd:element>

+        </xsd:choice>

+      </xsd:complexType>

+    </xsd:element>

+  </xsd:schema>

+  <resheader name="resmimetype">

+    <value>text/microsoft-resx</value>

+  </resheader>

+  <resheader name="version">

+    <value>2.0</value>

+  </resheader>

+  <resheader name="reader">

+    <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+  <resheader name="writer">

+    <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+</root>
\ No newline at end of file
diff --git a/Source/DafnyMenu/Resources/Images.png b/Source/DafnyMenu/Resources/Images.png
new file mode 100644
index 00000000..51fe0d15
--- /dev/null
+++ b/Source/DafnyMenu/Resources/Images.png
diff --git a/Source/DafnyMenu/Resources/Package.ico b/Source/DafnyMenu/Resources/Package.ico
new file mode 100644
index 00000000..449296f4
--- /dev/null
+++ b/Source/DafnyMenu/Resources/Package.ico
diff --git a/Source/DafnyMenu/VSPackage.resx b/Source/DafnyMenu/VSPackage.resx
new file mode 100644
index 00000000..8ab9cc50
--- /dev/null
+++ b/Source/DafnyMenu/VSPackage.resx
@@ -0,0 +1,140 @@
+<?xml version="1.0" encoding="utf-8"?>

+<!--

+    VS SDK Notes: This resx file contains the resources that will be consumed from your package by Visual Studio.

+    For example, Visual Studio will attempt to load resource '400' from this resource stream when it needs to

+    load your package's icon. Because Visual Studio will always look in the VSPackage.resources stream first for

+    resources it needs, you should put additional resources that Visual Studio will load directly into this resx 

+    file. 

+

+    Resources that you would like to access directly from your package in a strong-typed fashion should be stored 

+    in Resources.resx or another resx file.

+-->

+<root>

+  <!-- 

+    Microsoft ResX Schema 

+    

+    Version 2.0

+    

+    The primary goals of this format is to allow a simple XML format 

+    that is mostly human readable. The generation and parsing of the 

+    various data types are done through the TypeConverter classes 

+    associated with the data types.

+    

+    Example:

+    

+    ... ado.net/XML headers & schema ...

+    <resheader name="resmimetype">text/microsoft-resx</resheader>

+    <resheader name="version">2.0</resheader>

+    <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader>

+    <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader>

+    <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data>

+    <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data>

+    <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64">

+        <value>[base64 mime encoded serialized .NET Framework object]</value>

+    </data>

+    <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">

+        <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value>

+        <comment>This is a comment</comment>

+    </data>

+                

+    There are any number of "resheader" rows that contain simple 

+    name/value pairs.

+    

+    Each data row contains a name, and value. The row also contains a 

+    type or mimetype. Type corresponds to a .NET class that support 

+    text/value conversion through the TypeConverter architecture. 

+    Classes that don't support this are serialized and stored with the 

+    mimetype set.

+    

+    The mimetype is used for serialized objects, and tells the 

+    ResXResourceReader how to depersist the object. This is currently not 

+    extensible. For a given mimetype the value must be set accordingly:

+    

+    Note - application/x-microsoft.net.object.binary.base64 is the format 

+    that the ResXResourceWriter will generate, however the reader can 

+    read any of the formats listed below.

+    

+    mimetype: application/x-microsoft.net.object.binary.base64

+    value   : The object must be serialized with 

+            : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter

+            : and then encoded with base64 encoding.

+    

+    mimetype: application/x-microsoft.net.object.soap.base64

+    value   : The object must be serialized with 

+            : System.Runtime.Serialization.Formatters.Soap.SoapFormatter

+            : and then encoded with base64 encoding.

+

+    mimetype: application/x-microsoft.net.object.bytearray.base64

+    value   : The object must be serialized into a byte array 

+            : using a System.ComponentModel.TypeConverter

+            : and then encoded with base64 encoding.

+    -->

+  <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata">

+    <xsd:import namespace="http://www.w3.org/XML/1998/namespace" />

+    <xsd:element name="root" msdata:IsDataSet="true">

+      <xsd:complexType>

+        <xsd:choice maxOccurs="unbounded">

+          <xsd:element name="metadata">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" />

+              </xsd:sequence>

+              <xsd:attribute name="name" use="required" type="xsd:string" />

+              <xsd:attribute name="type" type="xsd:string" />

+              <xsd:attribute name="mimetype" type="xsd:string" />

+              <xsd:attribute ref="xml:space" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="assembly">

+            <xsd:complexType>

+              <xsd:attribute name="alias" type="xsd:string" />

+              <xsd:attribute name="name" type="xsd:string" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="data">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+                <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" />

+              <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" />

+              <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" />

+              <xsd:attribute ref="xml:space" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="resheader">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" use="required" />

+            </xsd:complexType>

+          </xsd:element>

+        </xsd:choice>

+      </xsd:complexType>

+    </xsd:element>

+  </xsd:schema>

+  <resheader name="resmimetype">

+    <value>text/microsoft-resx</value>

+  </resheader>

+  <resheader name="version">

+    <value>2.0</value>

+  </resheader>

+  <resheader name="reader">

+    <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+  <resheader name="writer">

+    <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+  <assembly alias="System.Windows.Forms" name="System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089" />

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

+  <data name="400" type="System.Resources.ResXFileRef, System.Windows.Forms">

+    <value>Resources\Package.ico;System.Drawing.Icon, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a</value>

+  </data>

+</root>
\ No newline at end of file
diff --git a/Source/DafnyMenu/source.extension.vsixmanifest b/Source/DafnyMenu/source.extension.vsixmanifest
new file mode 100644
index 00000000..08ea6bef
--- /dev/null
+++ b/Source/DafnyMenu/source.extension.vsixmanifest
@@ -0,0 +1,18 @@
+<?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="e1baf989-88a6-4acf-8d97-e0dc243476aa" Version="1.0" Language="en-US" Publisher="Microsoft Research" />

+    <DisplayName>DafnyMenu</DisplayName>

+    <Description xml:space="preserve">This is a menu for interacting with Dafny.</Description>

+  </Metadata>

+  <Installation InstalledByMsi="false">

+    <InstallationTarget Id="Microsoft.VisualStudio.Pro" Version="11.0" />

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

+  </Assets>

+</PackageManifest>