src/Pure/GUI/gui.scala
changeset 62113 16de2a9b5b3d
parent 61742 fd3b214b0979
child 63420 b43a3f7d9935
--- a/src/Pure/GUI/gui.scala	Sat Jan 09 20:56:00 2016 +0100
+++ b/src/Pure/GUI/gui.scala	Sat Jan 09 22:00:22 2016 +0100
@@ -166,7 +166,7 @@
 
   def tooltip_lines(text: String): String =
     if (text == null || text == "") null
-    else "<html>" + HTML.encode(text) + "</html>"
+    else "<html>" + HTML.output(text) + "</html>"
 
 
   /* icon */