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

1 files changed, 17 insertions, 0 deletions

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

   }

 }