Display values in the state list

2 files changed, 28 insertions, 7 deletions

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 312a2766..fb54aa2c 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -62,6 +62,7 @@
       this.currentStateView.DrawColumnHeader += new System.Windows.Forms.DrawListViewColumnHeaderEventHandler(this.listView1_DrawColumnHeader);

       this.currentStateView.DrawItem += new System.Windows.Forms.DrawListViewItemEventHandler(this.listView1_DrawItem);

       this.currentStateView.DrawSubItem += new System.Windows.Forms.DrawListViewSubItemEventHandler(this.listView1_DrawSubItem);

+      this.currentStateView.SelectedIndexChanged += new System.EventHandler(this.currentStateView_SelectedIndexChanged);

       this.currentStateView.MouseMove += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseMove);

       this.currentStateView.MouseUp += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseUp);

       this.currentStateView.Resize += new System.EventHandler(this.listView1_Resize);

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 2a53f72e..985d0211 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -224,6 +224,20 @@ namespace Microsoft.Boogie.ModelViewer
       var sel = stateList.SelectedItems[0].Index;

       SetState(sel);

     }

+

+    private void currentStateView_SelectedIndexChanged(object sender, EventArgs e)

+    {

+      if (currentStateView.SelectedItems.Count == 0) return;

+      var sel = (DisplayItem) currentStateView.SelectedItems[0];

+

+      stateList.BeginUpdate();

+      for (int i = 0; i < sel.skel.displayNodes.Length; ++i) {

+        var dn = sel.skel.displayNodes[i];

+        stateList.Items[i].SubItems[1].Text = DisplayItem.ValuesAsString(dn);

+      }

+      stateList.EndUpdate();

+    }

+

   }

 

   internal class SkeletonItem

@@ -345,20 +359,26 @@ namespace Microsoft.Boogie.ModelViewer
       }

 

       this.SubItems[0].Text = dispNode.Name;

+      this.SubItems[1].Text = ValuesAsString(dispNode).ToString();

+    }

+

+    internal DisplayItem()

+       : base(new string[] { "", "" })

+    {

+    }

+

+    static internal string ValuesAsString(IDisplayNode dn)

+    {

+      if (dn == null) return "";

 

       var sb = new StringBuilder();

-      foreach (var n in dispNode.Values) {

+      foreach (var n in dn.Values) {

         sb.Append(n).Append(", ");

         if (sb.Length > 300)

           break;

       }

       if (sb.Length > 2) sb.Length -= 2;

-      this.SubItems[1].Text = sb.ToString();

-    }

-

-    internal DisplayItem()

-       : base(new string[] { "", "" })

-    {

+      return sb.ToString();

     }

   }

 }