recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala Sat Nov 24 16:13:21 2012 +0100
1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala Sat Nov 24 16:24:39 2012 +0100
1.3 @@ -47,6 +47,13 @@
1.4 ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])
1.5
1.6
1.7 + /* basic tooltips, with multi-line support */
1.8 +
1.9 + def wrap_tooltip(text: String): String =
1.10 + if (text == "") null
1.11 + else "<html><pre>" + HTML.encode(text) + "</pre></html>"
1.12 +
1.13 +
1.14 /* buffers */
1.15
1.16 def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
2.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Nov 24 16:13:21 2012 +0100
2.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Nov 24 16:24:39 2012 +0100
2.3 @@ -31,8 +31,9 @@
2.4 Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
2.5 action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
2.6 tooltip =
2.7 - symbol +
2.8 - (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "")
2.9 + JEdit_Lib.wrap_tooltip(
2.10 + symbol +
2.11 + (if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else ""))
2.12 }
2.13
2.14 val group_tabs: TabbedPane = new TabbedPane {