--- 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><pre>" + HTML.encode(cat_lines(lines)) + "</pre></html>"
+
+
/* screen resolution */
def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
--- 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><pre>" + HTML.encode(text) + "</pre></html>"
-
-
/* buffers */
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
--- 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