diff options
| author |  MichalMoskal <unknown> | 2011-01-13 01:47:47 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-01-13 01:47:47 +0000 |
| commit | 979fef05165a95fc2911ce536e4b54d52584aade (patch) | |
| tree | 0d8c6ec3a062d6049b676d289779db584751ed59 /Source/ModelViewer | |
| parent | 4a3b3e6d50109c4f39c33f8d5af68d329e2b1354 (diff) | |
Display full name of node in tooltip
Diffstat (limited to 'Source/ModelViewer')
| -rw-r--r-- | Source/ModelViewer/Main.cs | 29 |
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;
|