# HG changeset patch # User wenzelm # Date 1353770679 -3600 # Node ID f83cab68c788b0aba69558b41b4c8963e8459a6c # Parent 820673500454d5961af8b1403a4416c1639826bb recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode; diff -r 820673500454 -r f83cab68c788 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Sat Nov 24 16:13:21 2012 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Sat Nov 24 16:24:39 2012 +0100 @@ -47,6 +47,13 @@ ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame]) + /* 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 820673500454 -r f83cab68c788 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Nov 24 16:13:21 2012 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Nov 24 16:24:39 2012 +0100 @@ -31,8 +31,9 @@ Font.PLAIN, Isabelle.font_size("jedit_font_scale").round) action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus } tooltip = - symbol + - (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "") + JEdit_Lib.wrap_tooltip( + symbol + + (if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else "")) } val group_tabs: TabbedPane = new TabbedPane {