# HG changeset patch # User wenzelm # Date 1379868138 -7200 # Node ID 064cb0458071e880a63f8a1383d3798326dd1e94 # Parent e64edcc2f8bf94063aea3b34a400af6a95c89ffb tuned; diff -r e64edcc2f8bf -r 064cb0458071 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Sun Sep 22 18:36:22 2013 +0200 +++ b/src/Pure/GUI/gui.scala Sun Sep 22 18:42:18 2013 +0200 @@ -109,6 +109,13 @@ } + /* tooltip with multi-line support */ + + def tooltip_lines(lines: List[String]): String = + if (lines.isEmpty) null + else "
" + HTML.encode(cat_lines(lines)) + "
" + + /* screen resolution */ def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72 diff -r e64edcc2f8bf -r 064cb0458071 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Sun Sep 22 18:36:22 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Sun Sep 22 18:42:18 2013 +0200 @@ -92,13 +92,6 @@ } - /* basic tooltips, with multi-line support */ - - def wrap_tooltip(text: String): String = - if (text == "") null - else "
" + HTML.encode(text) + "
" - - /* buffers */ def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = diff -r e64edcc2f8bf -r 064cb0458071 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Sun Sep 22 18:36:22 2013 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Sun Sep 22 18:42:18 2013 +0200 @@ -41,9 +41,7 @@ else text_area.setSelectedText(decoded) text_area.requestFocus } - tooltip = - JEdit_Lib.wrap_tooltip( - cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a))) + tooltip = GUI.tooltip_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)) } private class Reset_Component extends Button