src/Tools/jEdit/src/jedit_lib.scala
changeset 50186 f83cab68c788
parent 50116 88b971fca902
child 50195 863b1dfc396c
     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 =