changeset 56622 | 891d1b8b64fb |
parent 54965 | a8af7a9c38d1 |
child 56752 | 72b4205f4de9 |
--- a/src/Pure/GUI/gui.scala Sat Apr 19 18:37:41 2014 +0200 +++ b/src/Pure/GUI/gui.scala Sat Apr 19 19:03:32 2014 +0200 @@ -137,9 +137,9 @@ /* tooltip with multi-line support */ - def tooltip_lines(lines: List[String]): String = - if (lines.isEmpty) null - else "<html><pre>" + HTML.encode(cat_lines(lines)) + "</pre></html>" + def tooltip_lines(text: String): String = + if (text == null || text == "") null + else "<html>" + HTML.encode(text) + "</html>" /* screen resolution */