recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
authorwenzelm
Sat Nov 24 16:24:39 2012 +0100 (2012-11-24)
changeset 50186f83cab68c788
parent 50185 820673500454
child 50187 b5a09812abc4
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/symbols_dockable.scala
     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 {