summaryrefslogtreecommitdiff
path: root/Source/ModelViewer
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2011-01-13 01:47:47 +0000
committerGravatar MichalMoskal <unknown>2011-01-13 01:47:47 +0000
commit979fef05165a95fc2911ce536e4b54d52584aade (patch)
tree0d8c6ec3a062d6049b676d289779db584751ed59 /Source/ModelViewer
parent4a3b3e6d50109c4f39c33f8d5af68d329e2b1354 (diff)
Display full name of node in tooltip
Diffstat (limited to 'Source/ModelViewer')
-rw-r--r--Source/ModelViewer/Main.cs29
1 files changed, 16 insertions, 13 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 4870c9be..c9b574e8 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -642,32 +642,35 @@ namespace Microsoft.Boogie.ModelViewer
dispNode = skel.displayNodes[stateId];
active = dispNode != null;
+ var closeStateId = stateId;
+
if (dispNode == null) {
- for (int i = stateId; i < skel.displayNodes.Length; ++i) {
- dispNode = skel.displayNodes[i];
- if (dispNode != null) break;
- }
- for (int i = stateId; i >= 0; --i) {
- if (dispNode != null) break;
- dispNode = skel.displayNodes[i];
+ while (closeStateId < skel.displayNodes.Length && skel.displayNodes[closeStateId] == null)
+ closeStateId++;
+ if (closeStateId >= skel.displayNodes.Length) {
+ closeStateId = stateId;
+ while (closeStateId >= 0 && skel.displayNodes[closeStateId] == null)
+ closeStateId--;
}
+ dispNode = skel.displayNodes[closeStateId];
}
+ var fullName = skel.LongName(closeStateId);
var tooltip = dispNode.ToolTip;
- var aliases = ""; // AliasesAsString(dispNode);
- if (IsMatchListItem)
- aliases = "";
+ if (tooltip == null)
+ tooltip = "";
+ if(tooltip.Length > 0 && tooltip[tooltip.Length - 1] != '\n')
+ tooltip += "\n";
+ tooltip += "Full name: " + fullName;
if (tooltip != null) {
this.ToolTipText = tooltip;
- } else {
- this.ToolTipText = aliases;
}
var name = dispNode.Name;
if (IsMatchListItem) {
Util.Assert(active);
- name = skel.LongName(stateId);
+ name = fullName;
}
this.SubItems[0].Text = name;