Changed BVD to display shortened names if they are unique.

4 files changed, 33 insertions, 4 deletions

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index c2d786fc..602df7aa 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -298,7 +298,8 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       foreach (var v in names) {

         if (dm.GetUserVariableName(v) != null) {

           var val = state.TryGet(v);

-          var vn = new VariableNode(this, v, val);

+          var shortName = Regex.Replace(v, @"#\d+$", "");

+          var vn = new VariableNode(this, v, val, names.Any(n => n != v && Regex.Replace(n, @"#\d+$", "") == shortName) ? v : shortName);

           vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);

           if (curVars.ContainsKey(v))

             dm.RegisterLocalValue(vn.Name, val);

@@ -316,7 +317,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
         if (n == -1) continue;

         string name = f.Name.Substring(0, n);

         if (!name.Contains('#')) continue;

-        yield return new VariableNode(this, name, f.GetConstant());

+        yield return new VariableNode(this, name, f.GetConstant(), name);

       }

     }

 

@@ -376,11 +377,12 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     public bool updatedHere;

     public string realName;

 

-    public VariableNode(StateNode par, string realName, Model.Element elt)

+    public VariableNode(StateNode par, string realName, Model.Element elt, string shortName)

       : base(par, realName, elt)

     {

       this.realName = realName;

       name = new EdgeName(vm.GetUserVariableName(realName));

+      ShortName = shortName;

     }

   }

 }

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index b6ec0bae..0b54e689 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -67,6 +67,8 @@ namespace Microsoft.Boogie.ModelViewer
     /// </summary>

     string Name { get; }

 

+    string ShortName { get; }

+

     NodeCategory Category { get; }

     string Value { get; }

     string ToolTip { get; }

@@ -163,6 +165,27 @@ namespace Microsoft.Boogie.ModelViewer
       get { return name.ToString(); }

     }

 

+    private string shortName;

+

+    public virtual string ShortName

+    {

+      get

+      {

+        if (shortName != null)

+        {

+          return shortName;

+        }

+        else

+        {

+          return name.ToString();

+        }

+      }

+      set

+      {

+        shortName = value;

+      }

+    }

+

     public virtual Model.Element Element

     {

       get { return element; }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index c15ea167..c5685194 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -821,6 +821,10 @@ namespace Microsoft.Boogie.ModelViewer
       }

 

       var name = dispNode.Name;

+      if (name != dispNode.ShortName)

+      {

+        name = dispNode.ShortName;

+      }

 

       if (IsMatchListItem) {

         Util.Assert(active);

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index b4540717..ae062c93 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -1517,7 +1517,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       this.realName = realName;

     }

 

-    public string ShortName

+    public override string ShortName

     {

       set { this.name = new EdgeName(value); }

       get { return this.name.ToString(); }