src/Pure/GUI/gui.scala
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 */