src/Pure/GUI/gui.scala
Sat, 19 Apr 2014 19:03:32 +0200 wenzelm clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
less more (0) -10 -1 tip