Changed BVD to display shortened names if they are unique.

1 files changed, 23 insertions, 0 deletions

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; }