diff options
| author |  MichalMoskal <unknown> | 2010-10-15 00:23:14 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2010-10-15 00:23:14 +0000 |
| commit | 2bd631d07570bf81611486d01bcd5a21dee2d2c9 (patch) | |
| tree | 7ed182d56576ecfea56f9e384058855d626aef7b /Source/ModelViewer/Main.cs | |
| parent | 9e1f99c02907899e6b37427567d62719e38dde5c (diff) | |
Make it display maps
Diffstat (limited to 'Source/ModelViewer/Main.cs')
| -rw-r--r-- | Source/ModelViewer/Main.cs | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 3b5efd0d..7e45a558 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -261,8 +261,16 @@ namespace Microsoft.Boogie.ModelViewer }
}
+ var tooltip = dispNode.ToolTip;
+ var values = ValuesAsString(dispNode);
+ if (tooltip != null) {
+ this.ToolTipText = tooltip;
+ } else {
+ this.ToolTipText = values;
+ }
+
this.SubItems[0].Text = dispNode.Name;
- this.SubItems[1].Text = ValuesAsString(dispNode).ToString();
+ this.SubItems[1].Text = values;
}
internal DisplayItem()
|