DafnyExtension: Made it display if a variable was updated in a given model state.

2 files changed, 6 insertions, 3 deletions

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 9d033c8c..625973ad 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -46,10 +46,11 @@ namespace DafnyLanguage
         string text = FixedHoverText;

         if (Variable != null)

         {

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

+          bool wasUpdated;

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

           if (value != null)

           {

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

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

           }

         }

         return text;

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 60174668..2ceaa91d 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -313,9 +313,10 @@ namespace DafnyLanguage.DafnyMenu
       }

     }

 

-    public string TryToLookupValueInCurrentModel(string name)

+    public string TryToLookupValueInCurrentModel(string name, out bool wasUpdated)

     {

       string result = null;

+      wasUpdated = false;

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

       {

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

@@ -323,6 +324,7 @@ namespace DafnyLanguage.DafnyMenu
         var v = s.Vars.FirstOrDefault(var => var.Name == name);

         if (v != null)

         {

+          wasUpdated = v.updatedHere;

           result = m.CanonicalName(v.Element);

         }

       }