tuned;
authorwenzelm
Sun Sep 22 18:42:18 2013 +0200 (2013-09-22)
changeset 53786064cb0458071
parent 53785 e64edcc2f8bf
child 53787 e64389fe2d2c
tuned;
src/Pure/GUI/gui.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/symbols_dockable.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Sun Sep 22 18:36:22 2013 +0200
     1.2 +++ b/src/Pure/GUI/gui.scala	Sun Sep 22 18:42:18 2013 +0200
     1.3 @@ -109,6 +109,13 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* tooltip with multi-line support */
     1.8 +
     1.9 +  def tooltip_lines(lines: List[String]): String =
    1.10 +    if (lines.isEmpty) null
    1.11 +    else "<html><pre>" + HTML.encode(cat_lines(lines)) + "</pre></html>"
    1.12 +
    1.13 +
    1.14    /* screen resolution */
    1.15  
    1.16    def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
     2.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Sep 22 18:36:22 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Sep 22 18:42:18 2013 +0200
     2.3 @@ -92,13 +92,6 @@
     2.4    }
     2.5  
     2.6  
     2.7 -  /* basic tooltips, with multi-line support */
     2.8 -
     2.9 -  def wrap_tooltip(text: String): String =
    2.10 -    if (text == "") null
    2.11 -    else "<html><pre>" + HTML.encode(text) + "</pre></html>"
    2.12 -
    2.13 -
    2.14    /* buffers */
    2.15  
    2.16    def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
     3.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Sun Sep 22 18:36:22 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sun Sep 22 18:42:18 2013 +0200
     3.3 @@ -41,9 +41,7 @@
     3.4          else text_area.setSelectedText(decoded)
     3.5          text_area.requestFocus
     3.6        }
     3.7 -    tooltip =
     3.8 -      JEdit_Lib.wrap_tooltip(
     3.9 -        cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
    3.10 +    tooltip = GUI.tooltip_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a))
    3.11    }
    3.12  
    3.13    private class Reset_Component extends Button