diff options
author | 2010-11-06 01:21:19 +0000 | |
---|---|---|
committer | 2010-11-06 01:21:19 +0000 | |
commit | 34e5dd6c2177a83159982aca6c025ef95474689c (patch) | |
tree | 203f65482b6cf549fb4153cbf9eda53ce41bd59f /Source/ModelViewer/Main.cs | |
parent | 6f9978cce118489f6f76d8c08321bae2b599d4e1 (diff) |
Right-click enable
Diffstat (limited to 'Source/ModelViewer/Main.cs')
-rw-r--r-- | Source/ModelViewer/Main.cs | 75 |
1 files changed, 58 insertions, 17 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 5bc18fb2..130c841f 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -226,7 +226,6 @@ namespace Microsoft.Boogie.ModelViewer private void SyncListView(IEnumerable<SkeletonItem> items, ListView listView, Action<DisplayItem, SkeletonItem> cb)
{
-
var ch = items.ToArray();
var missing = ch.Length - listView.Items.Count;
listView.BeginUpdate();
@@ -242,8 +241,8 @@ namespace Microsoft.Boogie.ModelViewer }
for (int i = 0; i < ch.Length; ++i) {
var di = (DisplayItem)listView.Items[i];
- di.Set(ch[i], currentState);
cb(di, ch[i]);
+ di.Set(ch[i], currentState);
}
listView.EndUpdate();
listView.Invalidate();
@@ -315,7 +314,7 @@ namespace Microsoft.Boogie.ModelViewer eltEq = langModel.FindElement(w.Substring(3));
if (eltEq == null) bad = true;
}
- } else if (w.StartsWith("ref:")) {
+ } else if (w.StartsWith("use:")) {
var e = langModel.FindElement(w.Substring(4));
if (e == null) bad = true;
else eltRef.Add(e);
@@ -332,7 +331,7 @@ namespace Microsoft.Boogie.ModelViewer if (eltEq == null && wordsA.Length == 0 && refsA.Length == 0)
bad = true;
- var changed = force;
+ var changed = true; // force;
var matches = new List<SkeletonItem>();
foreach (var s in allItems) {
@@ -363,10 +362,28 @@ namespace Microsoft.Boogie.ModelViewer {
if (matchesList.SelectedItems.Count == 0) return;
var sel = (DisplayItem) matchesList.SelectedItems[0];
- ExpandParents(sel.skel);
+ GotoNode(sel.skel);
+ }
+
+ private void linkLabel1_LinkClicked(object sender, LinkLabelLinkClickedEventArgs e)
+ {
+ foreach (DisplayItem it in matchesList.Items) {
+ ExpandParents(it.skel);
+ }
+ SyncCurrentStateView();
+ }
+
+ private void SetSearch(string text)
+ {
+ textBox1.Text = text;
+ }
+
+ private void GotoNode(SkeletonItem skel)
+ {
+ ExpandParents(skel);
SyncCurrentStateView();
foreach (DisplayItem it in currentStateView.Items) {
- if (it.skel == sel.skel) {
+ if (it.skel == skel) {
it.Selected = true;
currentStateView.EnsureVisible(it.Index);
break;
@@ -374,12 +391,42 @@ namespace Microsoft.Boogie.ModelViewer }
}
- private void linkLabel1_LinkClicked(object sender, LinkLabelLinkClickedEventArgs e)
+ private void stateViewMenu_Opening(object sender, CancelEventArgs e)
{
- foreach (DisplayItem it in matchesList.Items) {
- ExpandParents(it.skel);
+ IDisplayNode sel = null;
+ SkeletonItem skel = null;
+ if (currentStateView.SelectedItems.Count > 0) {
+ var it = currentStateView.SelectedItems[0];
+ sel = ((DisplayItem)it).dispNode;
+ skel = ((DisplayItem)it).skel;
+ }
+
+ var items = stateViewMenu.Items;
+ items.Clear();
+
+ if (sel == null) {
+ items.Add(new ToolStripMenuItem("Unavailable") { Enabled = false });
+ return;
+ }
+
+ var selName = langModel.CanonicalName(sel.Element);
+
+ items.Add("Find uses...", null, (s, _) => SetSearch("use:" + selName));
+ items.Add("Aliases...", null, (s, _) => SetSearch("eq:" + selName));
+
+ var words = new string[0];
+ var elts = new Model.Element[0];
+ var max = 10;
+ foreach (var s in allItems) {
+ if (s != skel && s.isPrimary[currentState] && s.MatchesWords(words, elts, sel.Element, currentState)) {
+ if (max-- < 0) {
+ items.Add(new ToolStripMenuItem("...") { Enabled = false });
+ break;
+ }
+ var tmp = s;
+ items.Add(" " + s.LongName(currentState), null, (x, _) => GotoNode(tmp));
+ }
}
- SyncCurrentStateView();
}
}
@@ -427,13 +474,7 @@ namespace Microsoft.Boogie.ModelViewer if (IsMatchListItem) {
Util.Assert(active);
- var parents = new List<IDisplayNode>();
- for (var curr = skel; curr != null; curr = curr.parent) {
- if (curr.parent != null) // skip the root
- parents.Add(curr.displayNodes[stateId]);
- }
- parents.Reverse();
- name = skel.main.langModel.PathName(parents);
+ name = skel.LongName(stateId);
}
this.SubItems[0].Text = name;
|