DafnyExtension: Added support for displaying values from the model as hover text.

3 files changed, 42 insertions, 4 deletions

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 837d48ed..ad2bea8b 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -95,7 +95,7 @@ namespace DafnyLanguage
           }

           yield return new TagSpan<DafnyTokenTag>(

             new SnapshotSpan(_snapshot, r.Start, r.Length),

-            new DafnyTokenTag(kind, r.HoverText));

+            new DafnyTokenTag(kind, r.HoverText, r.Variable));

         }

       }

     }

@@ -325,6 +325,7 @@ namespace DafnyLanguage
       public readonly string HoverText;

       public enum OccurrenceKind { Use, Definition, WildDefinition, AdditionalInformation }

       public readonly OccurrenceKind Kind;

+      public readonly IVariable Variable;

 

       static bool SurfaceSyntaxToken(Bpl.IToken tok) {

         Contract.Requires(tok != null);

@@ -383,6 +384,7 @@ namespace DafnyLanguage
             }

           }

         }

+        Variable = v;

         HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);

         Kind = !isDefinition ? OccurrenceKind.Use : VarDecl.HasWildcardName(v) ? OccurrenceKind.WildDefinition : OccurrenceKind.Definition;

       }

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index abe67751..9d033c8c 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -36,16 +36,35 @@ namespace DafnyLanguage
 

   public class DafnyTokenTag : ITag

   {

+    string FixedHoverText;

+    private Microsoft.Dafny.IVariable Variable;

     public DafnyTokenKind Kind { get; private set; }

-    public string HoverText { get; private set; }

+    public string HoverText

+    {

+      get

+      {

+        string text = FixedHoverText;

+        if (Variable != null)

+        {

+          var value = DafnyClassifier.DafnyMenuPackage.TryToLookupValueInCurrentModel(Variable.UniqueName);

+          if (value != null)

+          {

+            text = string.Format("{0} (value = {1})", text == null ? "" : text, value);

+          }

+        }

+        return text;

+      }

+    }

 

     public DafnyTokenTag(DafnyTokenKind kind) {

       this.Kind = kind;

     }

 

-    public DafnyTokenTag(DafnyTokenKind kind, string hoverText) {

+    public DafnyTokenTag(DafnyTokenKind kind, string fixedHoverText, Microsoft.Dafny.IVariable variable = null)

+    {

       this.Kind = kind;

-      this.HoverText = hoverText;

+      this.FixedHoverText = fixedHoverText;

+      this.Variable = variable;

     }

   }

 

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index e55a97aa..bf114971 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -2,6 +2,7 @@
 using System.ComponentModel.Design;

 using System.Diagnostics;

 using System.Globalization;

+using System.Linq;

 using System.Runtime.InteropServices;

 using Microsoft.VisualStudio.ComponentModelHost;

 using Microsoft.VisualStudio.Editor;

@@ -310,6 +311,22 @@ namespace DafnyLanguage.DafnyMenu
       }

     }

 

+    public string TryToLookupValueInCurrentModel(string name)

+    {

+      string result = null;

+      if (!BVDDisabled && BvdToolWindow.BVD.LangModel != null)

+      {

+        var m = BvdToolWindow.BVD.LangModel as Microsoft.Boogie.ModelViewer.Dafny.DafnyModel;

+        var s = m.states[BvdToolWindow.BVD.CurrentState];

+        var v = s.Vars.FirstOrDefault(var => var.Name == name);

+        if (v != null && v.Element.Kind != Microsoft.Boogie.Model.ElementKind.Uninterpreted)

+        {

+          result = v.Element.ToString();

+        }

+      }

+      return result;

+    }

+

     #endregion

   }

 }