diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-09-20 15:50:49 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-09-20 15:50:49 -0700 |
| commit | 709c38aca00cdc72cb2e0fedf9f14c940530fd9a (patch) | |
| tree | cf46f88cfa6fae761be62867dd6a5e6db8e45715 | |
| parent | 5da11a7db25352dc15b4cbc83afc350b0d6808b9 (diff) | |
Tree navigation with left/right arrow
| -rw-r--r-- | Source/ModelViewer/Main.Designer.cs | 13 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.cs | 30 |
2 files changed, 37 insertions, 6 deletions
diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs index 859aade9..91d526d2 100644 --- a/Source/ModelViewer/Main.Designer.cs +++ b/Source/ModelViewer/Main.Designer.cs @@ -103,6 +103,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.SelectedIndexChanged += new System.EventHandler(this.currentStateView_SelectedIndexChanged);
+ this.currentStateView.KeyDown += new System.Windows.Forms.KeyEventHandler(this.currentStateView_KeyDown);
this.currentStateView.MouseUp += new System.Windows.Forms.MouseEventHandler(this.listView1_MouseUp);
this.currentStateView.Resize += new System.EventHandler(this.listView1_Resize);
//
@@ -175,9 +176,9 @@ //
// matchesList
//
- this.matchesList.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)
- | System.Windows.Forms.AnchorStyles.Left)
- | System.Windows.Forms.AnchorStyles.Right)));
+ this.matchesList.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)
+ | System.Windows.Forms.AnchorStyles.Left)
+ | System.Windows.Forms.AnchorStyles.Right)));
this.matchesList.Columns.AddRange(new System.Windows.Forms.ColumnHeader[] {
this.columnHeader4,
this.columnHeader5});
@@ -233,9 +234,9 @@ //
// textBox1
//
- this.textBox1.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)
- | System.Windows.Forms.AnchorStyles.Left)
- | System.Windows.Forms.AnchorStyles.Right)));
+ this.textBox1.Anchor = ((System.Windows.Forms.AnchorStyles)((((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Bottom)
+ | System.Windows.Forms.AnchorStyles.Left)
+ | System.Windows.Forms.AnchorStyles.Right)));
this.textBox1.Location = new System.Drawing.Point(53, 3);
this.textBox1.Name = "textBox1";
this.textBox1.Size = new System.Drawing.Size(477, 20);
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index a4492c70..f67b8497 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -700,6 +700,36 @@ namespace Microsoft.Boogie.ModelViewer {
}
+
+ private void currentStateView_KeyDown(object sender, KeyEventArgs e)
+ {
+ var node = SelectedNode();
+ if (node == null) return;
+
+ if (e.KeyCode == Keys.Right && !node.skel.Expanded && node.skel.Expandable) {
+ node.skel.Expanded = true;
+ SyncCurrentStateView();
+ return;
+ }
+
+ if (e.KeyCode == Keys.Left) {
+ if (node.skel.Expanded) {
+ node.skel.Expanded = false;
+ SyncCurrentStateView();
+ return;
+ } else {
+ var par = node.skel.parent;
+ if (par != null && par.parent != null) {
+ // par.Expanded = false;
+ foreach (DisplayItem it in currentStateView.Items) {
+ it.Selected = it.skel == par;
+ it.Focused = it.skel == par;
+ }
+ SyncCurrentStateView();
+ }
+ }
+ }
+ }
}
internal class DisplayItem : ListViewItem
|