# HG changeset patch # User immler # Date 1353511276 -3600 # Node ID ab5272955b3b3d071eb7ac9f4a894ab7dfdc9ac7 # Parent e6121a825db8866bbe4ee49c5a95e82c884ded06 removed (unicode) tooltips: can not adjust font in basic swing tooltip diff -r e6121a825db8 -r ab5272955b3b src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 16:04:00 2012 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 16:21:16 2012 +0100 @@ -40,8 +40,7 @@ pages ++= (for ((group, symbols) <- Symbol.groups) yield { new TabbedPane.Page(group, - new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) }, - (symbols take 10 map Symbol.decode).mkString(" ")) + new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) }) }).toList.sortWith(_.title <= _.title) pages += new TabbedPane.Page("search", new BorderPanel { val search = new TextField(10)