Show previous state

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()