diff options
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 Binary files differnew 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 Binary files differnew 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>
|
