Merge

10 files changed, 159 insertions, 151 deletions

diff --git a/Binaries/PrepareDafnyZip.bat b/Binaries/PrepareDafnyZip.bat
index 3aede819..83aab1a9 100644
--- a/Binaries/PrepareDafnyZip.bat
+++ b/Binaries/PrepareDafnyZip.bat
@@ -9,20 +9,22 @@ if not exist %DEST_DIR% mkdir %DEST_DIR%
 for %%f in (
   AbsInt.dll                          AbsInt.pdb
   Basetypes.dll                       Basetypes.pdb
-  BVD.exe                             BVD.pdb
   CodeContractsExtender.dll           CodeContractsExtender.pdb
   Core.dll                            Core.pdb
   Dafny.exe                           Dafny.pdb
   DafnyPipeline.dll                   DafnyPipeline.pdb
   DafnyPrelude.bpl                    DafnyRuntime.cs
+  Doomed.dll                          Doomed.pdb
+  ExecutionEngine.dll                 ExecutionEngine.pdb
   Graph.dll                           Graph.pdb
+  Houdini.dll                         Houdini.dll
   Model.dll                           Model.pdb
   ParserHelper.dll                    ParserHelper.pdb
   Provers.SMTLib.dll                  Provers.SMTLib.pdb
   UnivBackPred2.smt2
   VCExpr.dll                          VCExpr.pdb
   VCGeneration.dll                    VCGeneration.pdb
-  ..\Source\DafnyExtension\bin\Debug\DafnyLanguageService.vsix
+  DafnyLanguageService.vsix
 ) do (
   copy %%f %DEST_DIR%
 )
diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 31e344a1..b9c95c85 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003" ToolsVersion="4.0">

   <PropertyGroup>

     <MinimumVisualStudioVersion>11.0</MinimumVisualStudioVersion>

@@ -80,9 +80,6 @@
     <Reference Include="Houdini">

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

     </Reference>

-    <Reference Include="Graph">

-      <HintPath>..\..\..\boogie\Binaries\Graph.dll</HintPath>

-    </Reference>

     <Reference Include="Model">

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

     </Reference>

@@ -157,6 +154,7 @@
     <Compile Include="TokenTagger.cs" />

     <Compile Include="ClassificationTagger.cs" />

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

+    <Compile Include="..\version.cs" />

   </ItemGroup>

   <ItemGroup>

     <Content Include="DafnyPrelude.bpl">

@@ -199,4 +197,4 @@ copy /y "..\Binaries\DafnyRuntime.cs" "$(ProjectDir)"</PreBuildEvent>
   <Target Name="AfterBuild">

   </Target>

   -->

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

diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs
index 76b0c10d..9029f019 100644
--- a/Source/DafnyExtension/ErrorModelTagger.cs
+++ b/Source/DafnyExtension/ErrorModelTagger.cs
@@ -86,7 +86,7 @@ namespace DafnyLanguage
       foreach (var tag in _aggregator.GetTags(spans))

       {

         var ertag = tag.Tag as DafnyErrorResolverTag;

-        if (ertag != null && ertag.Error.Model != null)

+        if (ertag != null && ertag.Error.ModelText != null)

         {

           NormalizedSnapshotSpanCollection normSpans = tag.Span.GetSpans(snapshot);

 

@@ -147,14 +147,19 @@ namespace DafnyLanguage
       }

     }

 

-    private static Ellipse CreateErrorStateAdornment(DafnyErrorStateResolverTag esrtag)

+    private static string ErrorStateToolTip(bool isSelected, string description)

+    {

+      return string.Format("{0}{1}", isSelected ? "unselect state" : "select state", !string.IsNullOrEmpty(description) ? " [" + description + "]" : "");

+    }

+

+    private Ellipse CreateErrorStateAdornment(DafnyErrorStateResolverTag esrtag)

     {

       var result = new Ellipse

       {

         Fill = Brushes.DodgerBlue,

         Height = 12.0,

         Width = 12.0,

-        ToolTip = "select state",

+        ToolTip = ErrorStateToolTip(false, esrtag.Description),

         StrokeThickness = 3.0,

         Stroke = Brushes.DodgerBlue,

         Cursor = Cursors.Arrow,

@@ -163,53 +168,59 @@ namespace DafnyLanguage
 

       esrtag.Error.StateChangeEvent += new DafnyError.StateChangeEventHandler((o) =>

       {

-        result.Visibility = esrtag.Error.IsSelected ? System.Windows.Visibility.Visible : System.Windows.Visibility.Collapsed;

-        var isSelected = esrtag.Error.IsSelected && esrtag.Error.SelectedStateId == esrtag.Id;

-        result.Stroke = isSelected ? Brushes.Black : Brushes.DodgerBlue;

-        result.ToolTip = isSelected ? "unselect state" : "select state";

-        if (isSelected)

-        {

-          esrtag.Error.SelectedStateAdornment = result;

-        }

+        _view.VisualElement.Dispatcher.Invoke(() =>

+          {

+            result.Visibility = esrtag.Error.IsSelected ? System.Windows.Visibility.Visible : System.Windows.Visibility.Collapsed;

+            var isSelected = esrtag.Error.IsSelected && esrtag.Error.SelectedStateId == esrtag.Id;

+            result.Stroke = isSelected ? Brushes.Black : Brushes.DodgerBlue;

+            if (isSelected)

+            {

+              result.ToolTip = ErrorStateToolTip(isSelected, esrtag.Description);

+              esrtag.Error.SelectedStateAdornment = result;

+            }

+          });

       });

 

       result.MouseDown += new MouseButtonEventHandler((s, e) =>

       {

-        if (!esrtag.Error.IsSelected) { return; }

-        if (esrtag.Error.SelectedStateAdornment == result)

-        {

-          // unselect it

-          esrtag.Error.SelectedStateAdornment = null;

-          esrtag.Error.SelectedStateId = -1;

-          result.Stroke = Brushes.DodgerBlue;

-          result.ToolTip = "select state";

-        }

-        else

-        {

-          // unselect the old one

-          if (esrtag.Error.SelectedStateAdornment != null)

-          {

-            esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue;

-            esrtag.Error.SelectedStateAdornment.ToolTip = "select state";

-            esrtag.Error.SelectedStateAdornment = null;

-            esrtag.Error.SelectedStateId = -1;

-          }

-

-          // select the new one

-          esrtag.Error.SelectedStateAdornment = result;

-          esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black;

-          esrtag.Error.SelectedStateAdornment.ToolTip = "unselect state";

-          esrtag.Error.SelectedStateId = esrtag.Id;

-          if (!string.IsNullOrEmpty(esrtag.Error.Model))

+        _view.VisualElement.Dispatcher.Invoke(() =>

           {

-            DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.Model, esrtag.Id);

-          }

-        }

+            if (!esrtag.Error.IsSelected) { return; }

+            if (esrtag.Error.SelectedStateAdornment == result)

+            {

+              // unselect it

+              esrtag.Error.SelectedStateAdornment = null;

+              esrtag.Error.SelectedStateId = -1;

+              result.Stroke = Brushes.DodgerBlue;

+              result.ToolTip = result.ToolTip.ToString().Replace("unselect", "select");

+            }

+            else

+            {

+              // unselect the old one

+              if (esrtag.Error.SelectedStateAdornment != null)

+              {

+                esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue;

+                esrtag.Error.SelectedStateAdornment.ToolTip = esrtag.Error.SelectedStateAdornment.ToolTip.ToString().Replace("unselect", "select");

+                esrtag.Error.SelectedStateAdornment = null;

+                esrtag.Error.SelectedStateId = -1;

+              }

+

+              // select the new one

+              esrtag.Error.SelectedStateAdornment = result;

+              esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black;

+              esrtag.Error.SelectedStateAdornment.ToolTip = ErrorStateToolTip(true, esrtag.Description);

+              esrtag.Error.SelectedStateId = esrtag.Id;

+              if (!string.IsNullOrEmpty(esrtag.Error.ModelText))

+              {

+                DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.ModelText, esrtag.Id);

+              }

+            }

+          });

       });

       return result;

     }

 

-    private static Ellipse CreateErrorAdornment(DafnyErrorResolverTag ertag)

+    private Ellipse CreateErrorAdornment(DafnyErrorResolverTag ertag)

     {

       var result = new Ellipse

       {

@@ -221,45 +232,52 @@ namespace DafnyLanguage
         Stroke = Brushes.Crimson,

         Cursor = Cursors.Arrow,

       };

+

       result.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));

       result.MouseDown += new MouseButtonEventHandler((s, e) =>

       {

-        if (ertag.Error.IsSelected)

-        {

-          // unselect it

-          var selErr = ertag.Error.SelectedError;

-          ertag.Error.SelectedError = null;

-          ertag.Error.SelectedStateId = -1;

-          selErr.Notify();

-          result.Stroke = Brushes.Crimson;

-          result.ToolTip = "select error";

-        }

-        else

-        {

-          // unselect the old one

-          if (ertag.Error.SelectedError != null)

+        _view.VisualElement.Dispatcher.Invoke(() =>

           {

-            var selErr = ertag.Error.SelectedError;

-            selErr.Adornment.Stroke = Brushes.Crimson;

-            selErr.Adornment.ToolTip = "select error";

-            ertag.Error.SelectedStateId = -1;

-            ertag.Error.SelectedError = null;

-            selErr.Notify();

-          }

-

-          // select the new one

-          ertag.Error.SelectedError = ertag.Error;

-          ertag.Error.Adornment = result;

-          ertag.Error.Adornment.Stroke = Brushes.Black;

-          ertag.Error.Adornment.ToolTip = "unselect error";

-          if (!string.IsNullOrEmpty(ertag.Error.Model))

-          {

-            // select the last error state

-            ertag.Error.SelectedStateId = ertag.Error.StateSpans.Count() - 1;

-            DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(ertag.Error.Model, ertag.Error.SelectedStateId);

-          }

-          ertag.Error.SelectedError.Notify();

-        }

+            if (ertag.Error.IsSelected)

+            {

+              // unselect it

+              var selErr = ertag.Error.SelectedError;

+              selErr.SelectedStateId = -1;

+              selErr.SelectedStateAdornment = null;

+              ertag.Error.SelectedError = null;

+              result.Stroke = Brushes.Crimson;

+              result.ToolTip = "select error";

+              selErr.Notify();

+            }

+            else

+            {

+              // unselect the old one

+              if (ertag.Error.SelectedError != null)

+              {

+                var selErr = ertag.Error.SelectedError;

+                selErr.SelectedStateId = -1;

+                selErr.SelectedStateAdornment = null;

+                selErr.Adornment.Stroke = Brushes.Crimson;

+                selErr.Adornment.ToolTip = "select error";

+                ertag.Error.SelectedError = null;

+                selErr.Notify();

+              }

+

+              // select the new one

+              ertag.Error.SelectedError = ertag.Error;

+              ertag.Error.Adornment = result;

+              ertag.Error.Adornment.Stroke = Brushes.Black;

+              ertag.Error.Adornment.ToolTip = "unselect error";

+              if (!string.IsNullOrEmpty(ertag.Error.ModelText))

+              {

+                // select the last error state

+                ertag.Error.SelectedStateId = ertag.Error.Model.States.Count() - 1;

+                ertag.Error.SelectedStateAdornment = null;

+                DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(ertag.Error.ModelText, ertag.Error.SelectedStateId);

+              }

+              ertag.Error.SelectedError.Notify();

+            }

+          });

       });

       return result;

     }

@@ -275,7 +293,10 @@ namespace DafnyLanguage
         if (spans.Count > 0)

         {

           SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);

-          chng(this, new SnapshotSpanEventArgs(span));

+          _view.VisualElement.Dispatcher.Invoke(() =>

+            {

+              chng(this, new SnapshotSpanEventArgs(span));

+            });

         }

       }

     }

diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index fc0c0d1d..59afc448 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -85,7 +85,7 @@ namespace DafnyLanguage
       return activeTextView != null

                     && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

                     && resolver.Program != null

-                    && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));

+                    && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.ModelText));

     }

 

     public void ShowErrorModel(IWpfTextView activeTextView)

@@ -94,14 +94,14 @@ namespace DafnyLanguage
       var show = activeTextView != null

                  && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

                  && resolver.Program != null

-                 && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));

+                 && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));

       if (show)

       {

-        var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));

+        var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));

 

         if (selectedError != null)

         {

-          DafnyMenuPackage.ShowErrorModelInBVD(selectedError.Model, selectedError.SelectedStateId);

+          DafnyMenuPackage.ShowErrorModelInBVD(selectedError.ModelText, selectedError.SelectedStateId);

         }

       }

     }

diff --git a/Source/DafnyExtension/Properties/AssemblyInfo.cs b/Source/DafnyExtension/Properties/AssemblyInfo.cs
index a9922c2f..02da8a8a 100644
--- a/Source/DafnyExtension/Properties/AssemblyInfo.cs
+++ b/Source/DafnyExtension/Properties/AssemblyInfo.cs
@@ -17,16 +17,3 @@ using System.Runtime.InteropServices;
 // to COM components.  If you need to access a type in this assembly from 

 // COM, set the ComVisible attribute to true on that type.

 [assembly: ComVisible(false)]

-

-// 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 Build and Revision Numbers 

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

-// [assembly: AssemblyVersion("1.0.*")]

-[assembly: AssemblyVersion("1.0.0.0")]

-[assembly: AssemblyFileVersion("1.0.0.0")]

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index b1187054..81346c77 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -96,11 +96,13 @@ namespace DafnyLanguage
     public readonly DafnyError Error;

     public readonly ITrackingSpan Span;

     public readonly int Id;

-    public DafnyErrorStateResolverTag(DafnyError error, ITrackingSpan span, int id)

+    public readonly string Description;

+    public DafnyErrorStateResolverTag(DafnyError error, ITrackingSpan span, int id, string description)

     {

       Error = error;

       Span = span;

       Id = id;

+      Description = description;

     }

   }

 

@@ -278,9 +280,12 @@ namespace DafnyLanguage
             for (int i = 0; i < err.StateSpans.Length; i++)

             {

               var span = err.StateSpans[i];

+              var name = err.Model.States.ToArray()[i].Name;

+              var descStart = name.LastIndexOf(": ") + 2;

+              var description = 1 < descStart ? name.Substring(descStart) : "";

               if (span != null)

               {

-                yield return new TagSpan<IDafnyResolverTag>(span.GetSpan(currentSnapshot), new DafnyErrorStateResolverTag(err, span, i));

+                yield return new TagSpan<IDafnyResolverTag>(span.GetSpan(currentSnapshot), new DafnyErrorStateResolverTag(err, span, i, description));

               }

             }

           }

@@ -471,46 +476,53 @@ namespace DafnyLanguage
     public readonly string Message;

     protected readonly ITextSnapshot Snapshot;

     public readonly ITrackingSpan Span;

-    public readonly string Model;

-    private ITrackingSpan[] _stateSpans;

-    public ITrackingSpan[] StateSpans

+    public readonly string ModelText;

+    public Microsoft.Boogie.Model _model;

+    public Microsoft.Boogie.Model Model

     {

       get

       {

-        if (!string.IsNullOrEmpty(Model))

+        if (_model == null && !string.IsNullOrEmpty(ModelText))

         {

-          if (_stateSpans != null) { return _stateSpans; }

-          var locRegex = new Regex(@"\((\d+),(\d+)\)");

-          using (var rd = new StringReader(Model))

+          using (var rd = new StringReader(ModelText))

           {

-            var model = Microsoft.Boogie.Model.ParseModels(rd, null).ToArray();

-            Contract.Assert(model.Length == 1);

-            _stateSpans = model[0].States.Select(

-              cs =>

-              {

-                var match = locRegex.Match(cs.Name);

-                if (!match.Success)

-                {

-                  return null;

-                }

-                else

-                {

-                  var line = Math.Max(0, int.Parse(match.Groups[1].Value) - 1);

-                  var column = Math.Max(0, int.Parse(match.Groups[2].Value) - 1);

-                  var sLine = Snapshot.GetLineFromLineNumber(line);

-                  Contract.Assert(column <= sLine.Length);

-                  var sLength = Math.Max(0, Math.Min(sLine.Length - column, 0));

-                  return Snapshot.CreateTrackingSpan(sLine.Start + column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);

-                }

-              }

-            ).ToArray();

-            return _stateSpans;

+            var models = Microsoft.Boogie.Model.ParseModels(rd, null).ToArray();

+            Contract.Assert(models.Length == 1);

+            _model = models[0];

           }

         }

-        else

-        {

-          return null;

+        return _model;

+      }

+    }

+    private ITrackingSpan[] _stateSpans;

+    public ITrackingSpan[] StateSpans

+    {

+      get

+      {

+        if (_stateSpans == null && Model != null)

+        {          

+          var model = Model;

+          var locRegex = new Regex(@"\((\d+),(\d+)\)");

+          _stateSpans = model.States.Select(

+           cs =>

+           {

+             var match = locRegex.Match(cs.Name);

+             if (!match.Success)

+             {

+               return null;

+             }

+             else

+             {

+               var line = Math.Max(0, int.Parse(match.Groups[1].Value) - 1);

+               var column = Math.Max(0, int.Parse(match.Groups[2].Value) - 1);

+               var sLine = Snapshot.GetLineFromLineNumber(line);

+               Contract.Assert(column <= sLine.Length);

+               var sLength = Math.Max(0, Math.Min(sLine.Length - column, 0));

+               return Snapshot.CreateTrackingSpan(sLine.Start + column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);

+             }

+           }).ToArray();

         }

+        return _stateSpans;

       }

     }

     public int SelectedStateId { get; set; }

@@ -561,7 +573,7 @@ namespace DafnyLanguage
       Contract.Assert(Column <= sLine.Length);

       var sLength = Math.Max(0, Math.Min(sLine.Length - Column, 5));

       Span = snapshot.CreateTrackingSpan(sLine.Start + Column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);

-      Model = model;

+      ModelText = model;

       _errorSelection = _errorSelectionSingleton;

       SelectedStateId = -1;

     }

diff --git a/Source/DafnyExtension/source.extension.vsixmanifest b/Source/DafnyExtension/source.extension.vsixmanifest
index 9fda1773..5654b6cd 100644
--- a/Source/DafnyExtension/source.extension.vsixmanifest
+++ b/Source/DafnyExtension/source.extension.vsixmanifest
@@ -1,7 +1,7 @@
 <?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="6c7ed99a-206a-4937-9e08-b389de175f68" Version="1.0" Language="en-US" Publisher="Microsoft Research" />

+    <Identity Id="6c7ed99a-206a-4937-9e08-b389de175f68" Version="1.6.3.00320" Language="en-US" Publisher="Microsoft Research" />

     <DisplayName>DafnyLanguageMode</DisplayName>

     <Description xml:space="preserve">This is a language mode for using the Dafny language inside Visual Studio.</Description>

   </Metadata>

diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
index 7e9fb302..a7679e04 100644
--- a/Source/DafnyMenu/DafnyMenu.csproj
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -106,6 +106,7 @@
     <Compile Include="GlobalSuppressions.cs" />

     <Compile Include="DafnyMenuPackage.cs" />

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

+    <Compile Include="..\version.cs" />

     <Compile Include="PkgCmdID.cs" />

   </ItemGroup>

   <ItemGroup>

diff --git a/Source/DafnyMenu/Properties/AssemblyInfo.cs b/Source/DafnyMenu/Properties/AssemblyInfo.cs
index b1a5687d..9ceb8360 100644
--- a/Source/DafnyMenu/Properties/AssemblyInfo.cs
+++ b/Source/DafnyMenu/Properties/AssemblyInfo.cs
@@ -17,16 +17,3 @@ using System.Runtime.InteropServices;
 [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/source.extension.vsixmanifest b/Source/DafnyMenu/source.extension.vsixmanifest
index 2e21caed..3ddc722c 100644
--- a/Source/DafnyMenu/source.extension.vsixmanifest
+++ b/Source/DafnyMenu/source.extension.vsixmanifest
@@ -1,7 +1,7 @@
 <?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" />

+    <Identity Id="e1baf989-88a6-4acf-8d97-e0dc243476aa" Version="1.6.3.00320" Language="en-US" Publisher="Microsoft Research" />

     <DisplayName>DafnyMenu</DisplayName>

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

   </Metadata>