diff options
| -rw-r--r-- | Source/ModelViewer/Main.Designer.cs | 1 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.cs | 34 |
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();
}
}
}
|