diff options
author | 2010-11-04 22:44:24 +0000 | |
---|---|---|
committer | 2010-11-04 22:44:24 +0000 | |
commit | c88ea367ad6ecee642ed5a42784e3e1b5cebcefe (patch) | |
tree | 4e503a8c294a275fe65302d16b385fe370c9b49c /Source/ModelViewer/Main.cs | |
parent | dcc5ed185677b6892591d242583dc0fd2c33a858 (diff) |
Add search facility
Diffstat (limited to 'Source/ModelViewer/Main.cs')
-rw-r--r-- | Source/ModelViewer/Main.cs | 149 |
1 files changed, 116 insertions, 33 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 79a1d63c..4e20c6ef 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -17,6 +17,7 @@ namespace Microsoft.Boogie.ModelViewer {
public string SearchText;
SkeletonItem unfoldingRoot;
+ SkeletonItem[] allItems;
int currentState;
IState[] states;
internal ILanguageProvider langProvider;
@@ -57,7 +58,7 @@ namespace Microsoft.Boogie.ModelViewer m = models[0];
}
- this.Text = Path.GetFileName(filename) + " - Boogie Model Viewer";
+ this.Text = Path.GetFileName(filename) + " - Boogie Verification Debugger";
langProvider = null;
foreach (var p in Providers()) {
@@ -70,7 +71,7 @@ namespace Microsoft.Boogie.ModelViewer var items = new List<ListViewItem>();
states = langProvider.GetStates(m).ToArray();
unfoldingRoot = new SkeletonItem(this, states.Length);
- unfoldingRoot.PopulateRoot(states);
+ allItems = unfoldingRoot.PopulateRoot(states);
var idx = 0;
foreach (var i in states) {
@@ -90,7 +91,7 @@ namespace Microsoft.Boogie.ModelViewer void SetState(int id)
{
currentState = id;
- SyncListView();
+ SyncCurrentStateView();
}
internal void Activate(TreeNode treeNode)
@@ -106,27 +107,42 @@ namespace Microsoft.Boogie.ModelViewer const int levelMult = 16;
const int plusWidth = 16;
+ static Color Col(int c)
+ {
+ return Color.FromArgb(c >> 16, (c >> 8) & 0xff, c & 0xff);
+ }
+
static StringFormat center = new StringFormat() { Alignment = StringAlignment.Center };
- static Pen plusPen = new Pen(Color.FromArgb(0xaa, 0xaa, 0xaa));
- static Brush grayedOut = new SolidBrush(Color.FromArgb(0xaa, 0xaa, 0xaa));
+ static Pen plusPen = new Pen(Col(0xaaaaaa));
+ static Brush grayedOut = new SolidBrush(Col(0xaaaaaa));
+ static Brush nonPrimary = new SolidBrush(Col(0xeeeeee));
+ static Brush matchBg = new SolidBrush(Col(0xFFFA6F));
private void listView1_DrawItem(object sender, DrawListViewItemEventArgs e)
{
var item = (DisplayItem)e.Item;
var skel = item.skel;
var rect = e.Bounds;
+ var listView = (ListView)sender;
rect.Y += 1;
rect.Height -= 2;
var textBrush = Brushes.Black;
- if (currentStateView.SelectedIndices.Count > 0 && currentStateView.SelectedIndices[0] == e.ItemIndex) {
+ if (listView.SelectedIndices.Count > 0 && listView.SelectedIndices[0] == e.ItemIndex) {
e.Graphics.FillRectangle(Brushes.Navy, rect);
textBrush = Brushes.White;
} else {
- e.Graphics.FillRectangle(Brushes.White, rect);
+ var bg = Brushes.White;
+ if (item.active && !skel.isPrimary[currentState])
+ bg = nonPrimary;
+ if (item.skel.isMatch)
+ bg = matchBg;
+ e.Graphics.FillRectangle(bg, rect);
}
var off = levelMult * item.skel.level;
+ if (item.IsMatchListItem)
+ off = 0;
{
var plusRect = rect;
@@ -149,23 +165,23 @@ namespace Microsoft.Boogie.ModelViewer off += plusWidth + 3;
var nameRect = rect;
- var font = currentStateView.Font;
+ var font = listView.Font;
if ((item.dispNode.State & NodeState.Changed) != 0)
textBrush = Brushes.Red;
if (!item.active)
textBrush = grayedOut;
- nameRect.Width = currentStateView.Columns[0].Width - 1 - off;
+ nameRect.Width = listView.Columns[0].Width - 1 - off;
nameRect.X += off;
- var width = DrawString(e.Graphics, item.dispNode.Name.ShortName(), font, textBrush, nameRect);
+ var width = DrawString(e.Graphics, item.SubItems[0].Text, font, textBrush, nameRect);
nameRect.X += width + 4;
- nameRect.Width = currentStateView.Columns[0].Width + currentStateView.Columns[1].Width - nameRect.X;
+ nameRect.Width = listView.Columns[0].Width + listView.Columns[1].Width - nameRect.X;
width = DrawString(e.Graphics, item.SubItems[1].Text, font, textBrush, nameRect);
nameRect.X += width + 4;
- nameRect.Width = currentStateView.Width - nameRect.X;
+ nameRect.Width = listView.Width - nameRect.X;
width = DrawString(e.Graphics, item.SubItems[2].Text, font, textBrush, nameRect);
}
@@ -179,20 +195,12 @@ namespace Microsoft.Boogie.ModelViewer return minRect.Width;
}
- private void listView1_DrawSubItem(object sender, DrawListViewSubItemEventArgs e)
- {
- }
-
private void listView1_DrawColumnHeader(object sender, DrawListViewColumnHeaderEventArgs e)
{
e.DrawBackground();
e.DrawText();
}
- private void listView1_MouseMove(object sender, MouseEventArgs e)
- {
- }
-
private void listView1_MouseUp(object sender, MouseEventArgs e)
{
var clickedItem = (DisplayItem)currentStateView.GetItemAt(5, e.Y);
@@ -204,31 +212,39 @@ namespace Microsoft.Boogie.ModelViewer int plusLoc = skel.level * levelMult;
if (skel.Expandable && e.X >= plusLoc && e.X <= plusLoc + plusWidth) {
skel.Expanded = !skel.Expanded;
- SyncListView();
+ SyncCurrentStateView();
}
}
}
- private void SyncListView()
+ private void SyncCurrentStateView()
+ {
+ SyncListView(unfoldingRoot.RecChildren, currentStateView, (x, y) => { });
+ }
+
+ private void SyncListView(IEnumerable<SkeletonItem> items, ListView listView, Action<DisplayItem, SkeletonItem> cb)
{
- var ch = unfoldingRoot.RecChildren.ToArray();
- var missing = ch.Length - currentStateView.Items.Count;
- currentStateView.BeginUpdate();
+ var ch = items.ToArray();
+ var missing = ch.Length - listView.Items.Count;
+ listView.BeginUpdate();
if (missing < 0) {
missing = -missing;
while (missing-- > 0) {
- currentStateView.Items.RemoveAt(currentStateView.Items.Count - 1);
+ listView.Items.RemoveAt(listView.Items.Count - 1);
}
} else {
while (missing-- > 0) {
- currentStateView.Items.Add(new DisplayItem());
+ listView.Items.Add(new DisplayItem());
}
}
- for (int i = 0; i < ch.Length; ++i)
- ((DisplayItem)currentStateView.Items[i]).Set(ch[i], currentState);
- currentStateView.EndUpdate();
- currentStateView.Invalidate();
+ for (int i = 0; i < ch.Length; ++i) {
+ var di = (DisplayItem)listView.Items[i];
+ di.Set(ch[i], currentState);
+ cb(di, ch[i]);
+ }
+ listView.EndUpdate();
+ listView.Invalidate();
}
private void listView1_ColumnWidthChanged(object sender, ColumnWidthChangedEventArgs e)
@@ -268,6 +284,70 @@ namespace Microsoft.Boogie.ModelViewer stateList.EndUpdate();
}
+ private void ExpandParents(SkeletonItem item)
+ {
+ item = item.parent;
+ while (item != null && !item.Expanded) {
+ item.Expanded = true;
+ item = item.parent;
+ }
+ }
+
+ private void textBox1_TextChanged(object sender, EventArgs e)
+ {
+ UpdateMatches(false);
+ }
+
+ private void UpdateMatches(bool force)
+ {
+ var words = textBox1.Text.Split(' ').Where(s => s != "").Select(s => s.ToLower()).ToArray();
+ var changed = force;
+ var matches = new List<SkeletonItem>();
+ foreach (var s in allItems) {
+ var newMatch = false;
+ if (s.isPrimary[currentState] && words.Length > 0) {
+ newMatch = s.MatchesWords(words, currentState);
+ }
+ if (newMatch)
+ matches.Add(s);
+ if (s.isMatch != newMatch) {
+ changed = true;
+ s.isMatch = newMatch;
+ }
+ }
+
+ if (changed) {
+ SyncListView(matches, matchesList, (di, _) => { di.IsMatchListItem = true; });
+ }
+ }
+
+ private void matchesList_Resize(object sender, EventArgs e)
+ {
+ matchesList.Invalidate();
+ }
+
+ private void matchesList_DoubleClick(object sender, EventArgs e)
+ {
+ if (matchesList.SelectedItems.Count == 0) return;
+ var sel = (DisplayItem) matchesList.SelectedItems[0];
+ ExpandParents(sel.skel);
+ SyncCurrentStateView();
+ foreach (DisplayItem it in currentStateView.Items) {
+ if (it.skel == sel.skel) {
+ it.Selected = true;
+ currentStateView.EnsureVisible(it.Index);
+ break;
+ }
+ }
+ }
+
+ private void linkLabel1_LinkClicked(object sender, LinkLabelLinkClickedEventArgs e)
+ {
+ foreach (DisplayItem it in matchesList.Items) {
+ ExpandParents(it.skel);
+ }
+ SyncCurrentStateView();
+ }
}
internal class DisplayItem : ListViewItem
@@ -277,6 +357,8 @@ namespace Microsoft.Boogie.ModelViewer internal bool active;
internal IDisplayNode dispNode;
+ public bool IsMatchListItem { get; set; }
+
internal void Set(SkeletonItem s, int id)
{
if (skel == s && stateId == id)
@@ -300,16 +382,17 @@ namespace Microsoft.Boogie.ModelViewer var tooltip = dispNode.ToolTip;
var aliases = AliasesAsString(dispNode);
+ if (IsMatchListItem)
+ aliases = "";
if (tooltip != null) {
this.ToolTipText = tooltip;
} else {
this.ToolTipText = aliases;
}
- this.SubItems[0].Text = dispNode.Name.ShortName();
+ this.SubItems[0].Text = IsMatchListItem ? dispNode.Name.FullName() : dispNode.Name.ShortName();
this.SubItems[1].Text = active ? dispNode.CanonicalValue : "";
this.SubItems[2].Text = active ? aliases : "";
-
}
internal DisplayItem()
|