src/Tools/jEdit/src/symbols_dockable.scala
changeset 53786 064cb0458071
parent 53713 bb15972a644d
child 55825 694833e3e4a0
     1.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Sun Sep 22 18:36:22 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sun Sep 22 18:42:18 2013 +0200
     1.3 @@ -41,9 +41,7 @@
     1.4          else text_area.setSelectedText(decoded)
     1.5          text_area.requestFocus
     1.6        }
     1.7 -    tooltip =
     1.8 -      JEdit_Lib.wrap_tooltip(
     1.9 -        cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
    1.10 +    tooltip = GUI.tooltip_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a))
    1.11    }
    1.12  
    1.13    private class Reset_Component extends Button