From 91b08ecb702cc49e29094b938e943a51087c00a4 Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Sat, 6 Nov 2010 01:21:35 +0000 Subject: Show previous state --- Source/ModelViewer/Main.Designer.cs | 25 ++++++++--------- Source/ModelViewer/Main.cs | 56 ++++++++++++++++++++++++++++--------- 2 files changed, 55 insertions(+), 26 deletions(-) diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs index 9932a550..fc3c5291 100644 --- a/Source/ModelViewer/Main.Designer.cs +++ b/Source/ModelViewer/Main.Designer.cs @@ -74,7 +74,7 @@ this.currentStateView.Name = "currentStateView"; this.currentStateView.OwnerDraw = true; this.currentStateView.ShowItemToolTips = true; - this.currentStateView.Size = new System.Drawing.Size(677, 558); + this.currentStateView.Size = new System.Drawing.Size(596, 558); this.currentStateView.TabIndex = 0; this.currentStateView.UseCompatibleStateImageBehavior = false; this.currentStateView.View = System.Windows.Forms.View.Details; @@ -88,17 +88,17 @@ // name // this.name.Text = "Name"; - this.name.Width = 174; + this.name.Width = 298; // // value // this.value.Text = "Value"; - this.value.Width = 99; + this.value.Width = 126; // // prevValue // this.prevValue.Text = "Previous"; - this.prevValue.Width = 147; + this.prevValue.Width = 62; // // stateViewMenu // @@ -128,7 +128,7 @@ // this.splitContainer1.Panel2.Controls.Add(this.stateList); this.splitContainer1.Size = new System.Drawing.Size(915, 726); - this.splitContainer1.SplitterDistance = 677; + this.splitContainer1.SplitterDistance = 596; this.splitContainer1.TabIndex = 1; // // splitContainer2 @@ -148,7 +148,7 @@ this.splitContainer2.Panel2.Controls.Add(this.linkLabel1); this.splitContainer2.Panel2.Controls.Add(this.label1); this.splitContainer2.Panel2.Controls.Add(this.textBox1); - this.splitContainer2.Size = new System.Drawing.Size(677, 726); + this.splitContainer2.Size = new System.Drawing.Size(596, 726); this.splitContainer2.SplitterDistance = 558; this.splitContainer2.TabIndex = 1; // @@ -168,7 +168,7 @@ this.matchesList.Name = "matchesList"; this.matchesList.OwnerDraw = true; this.matchesList.ShowItemToolTips = true; - this.matchesList.Size = new System.Drawing.Size(677, 135); + this.matchesList.Size = new System.Drawing.Size(596, 135); this.matchesList.TabIndex = 4; this.matchesList.UseCompatibleStateImageBehavior = false; this.matchesList.View = System.Windows.Forms.View.Details; @@ -186,13 +186,13 @@ // columnHeader5 // this.columnHeader5.Text = "Value"; - this.columnHeader5.Width = 350; + this.columnHeader5.Width = 250; // // linkLabel1 // this.linkLabel1.Anchor = ((System.Windows.Forms.AnchorStyles)((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Right))); this.linkLabel1.AutoSize = true; - this.linkLabel1.Location = new System.Drawing.Point(617, 5); + this.linkLabel1.Location = new System.Drawing.Point(536, 5); this.linkLabel1.Name = "linkLabel1"; this.linkLabel1.Size = new System.Drawing.Size(57, 13); this.linkLabel1.TabIndex = 3; @@ -217,7 +217,7 @@ | 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(558, 20); + this.textBox1.Size = new System.Drawing.Size(477, 20); this.textBox1.TabIndex = 1; this.textBox1.TextChanged += new System.EventHandler(this.textBox1_TextChanged); // @@ -231,12 +231,11 @@ this.stateList.FullRowSelect = true; this.stateList.GridLines = true; this.stateList.HeaderStyle = System.Windows.Forms.ColumnHeaderStyle.Nonclickable; - this.stateList.HideSelection = false; this.stateList.Location = new System.Drawing.Point(0, 0); this.stateList.MultiSelect = false; this.stateList.Name = "stateList"; this.stateList.ShowItemToolTips = true; - this.stateList.Size = new System.Drawing.Size(234, 726); + this.stateList.Size = new System.Drawing.Size(315, 726); this.stateList.TabIndex = 0; this.stateList.UseCompatibleStateImageBehavior = false; this.stateList.View = System.Windows.Forms.View.Details; @@ -250,7 +249,7 @@ // columnHeader1 // this.columnHeader1.Text = "State"; - this.columnHeader1.Width = 109; + this.columnHeader1.Width = 169; // // columnHeader2 // diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 130c841f..77ebb1a3 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -18,7 +18,7 @@ namespace Microsoft.Boogie.ModelViewer public string SearchText; SkeletonItem unfoldingRoot; SkeletonItem[] allItems; - int currentState; + int currentState, previousState = -1; IState[] states; internal ILanguageProvider langProvider; internal ILanguageSpecificModel langModel; @@ -86,13 +86,21 @@ namespace Microsoft.Boogie.ModelViewer unfoldingRoot.Expanded = true; SetState(0); stateList.Items[0].Selected = true; + SetColumnSizes(); + } - currentStateView.Columns[2].Width = currentStateView.Width - currentStateView.Columns[0].Width - currentStateView.Columns[1].Width - 5; + private void SetColumnSizes() + { + currentStateView.Columns[0].Width = currentStateView.Width - currentStateView.Columns[1].Width - currentStateView.Columns[2].Width - 5; + stateList.Columns[1].Width = stateList.Width - stateList.Columns[0].Width - stateList.Columns[2].Width - 5; } void SetState(int id) { - currentState = id; + if (currentState != id) { + previousState = currentState; + currentState = id; + } UpdateMatches(true); } @@ -119,6 +127,10 @@ namespace Microsoft.Boogie.ModelViewer static Brush grayedOut = new SolidBrush(Col(0xaaaaaa)); static Brush nonPrimary = new SolidBrush(Col(0xeeeeee)); static Brush matchBg = new SolidBrush(Col(0xFFFA6F)); + + static SolidBrush regularStateBrush = new SolidBrush(Color.Black); + static SolidBrush previousStateBrush = new SolidBrush(Color.Blue); + static SolidBrush currentStateBrush = new SolidBrush(Color.Red); private void listView1_DrawItem(object sender, DrawListViewItemEventArgs e) { @@ -184,7 +196,8 @@ namespace Microsoft.Boogie.ModelViewer nameRect.X += width + 4; nameRect.Width = listView.Width - nameRect.X; - width = DrawString(e.Graphics, item.SubItems[2].Text, font, textBrush, nameRect); + var t = item.SubItems[2].Text; + width = DrawString(e.Graphics, t, font, t == item.SubItems[1].Text ? grayedOut : previousStateBrush, nameRect); } private int DrawString(Graphics g, string s, Font font, Brush textBrush, Rectangle minRect) @@ -200,7 +213,16 @@ namespace Microsoft.Boogie.ModelViewer private void listView1_DrawColumnHeader(object sender, DrawListViewColumnHeaderEventArgs e) { e.DrawBackground(); - e.DrawText(); + var brush = regularStateBrush; + if (e.Header.Index == 1) + brush = currentStateBrush; + else if (e.Header.Index == 2) + brush = previousStateBrush; + + Rectangle r = e.Bounds; + r.X += 5; + r.Y += 4; + DrawString(e.Graphics, e.Header.Text, e.Header.ListView.Font, brush, r); } private void listView1_MouseUp(object sender, MouseEventArgs e) @@ -242,7 +264,7 @@ namespace Microsoft.Boogie.ModelViewer for (int i = 0; i < ch.Length; ++i) { var di = (DisplayItem)listView.Items[i]; cb(di, ch[i]); - di.Set(ch[i], currentState); + di.Set(ch[i], currentState, previousState); } listView.EndUpdate(); listView.Invalidate(); @@ -255,6 +277,7 @@ namespace Microsoft.Boogie.ModelViewer private void listView1_Resize(object sender, EventArgs e) { + SetColumnSizes(); currentStateView.Invalidate(); } @@ -264,10 +287,10 @@ namespace Microsoft.Boogie.ModelViewer if (stateList.SelectedItems.Count == 0) return; var sel = stateList.SelectedItems[0].Index; - var normalFont = stateList.Font; - var boldFont = new Font(normalFont, FontStyle.Bold); - stateList.Items[currentState].Font = normalFont; - stateList.Items[sel].Font = boldFont; + if (previousState >= 0) + stateList.Items[previousState].ForeColor = regularStateBrush.Color; + stateList.Items[currentState].ForeColor = previousStateBrush.Color; + stateList.Items[sel].ForeColor = currentStateBrush.Color; SetState(sel); } @@ -439,7 +462,7 @@ namespace Microsoft.Boogie.ModelViewer public bool IsMatchListItem { get; set; } - internal void Set(SkeletonItem s, int id) + internal void Set(SkeletonItem s, int id, int prevId) { if (skel == s && stateId == id) return; @@ -474,12 +497,19 @@ namespace Microsoft.Boogie.ModelViewer if (IsMatchListItem) { Util.Assert(active); - name = skel.LongName(stateId); + name = skel.LongName(stateId); } this.SubItems[0].Text = name; this.SubItems[1].Text = active ? dispNode.Value : ""; - // this.SubItems[2].Text = active ? aliases : ""; + + var prev = ""; + + if (!IsMatchListItem && prevId > 0 && skel.displayNodes[prevId] != null) { + prev = skel.displayNodes[prevId].Value; + } + + this.SubItems[2].Text = prev; } internal DisplayItem() -- cgit v1.2.3