1.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 16:04:00 2012 +0100
1.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 16:21:16 2012 +0100
1.3 @@ -40,8 +40,7 @@
1.4 pages ++= (for ((group, symbols) <- Symbol.groups) yield
1.5 {
1.6 new TabbedPane.Page(group,
1.7 - new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) },
1.8 - (symbols take 10 map Symbol.decode).mkString(" "))
1.9 + new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) })
1.10 }).toList.sortWith(_.title <= _.title)
1.11 pages += new TabbedPane.Page("search", new BorderPanel {
1.12 val search = new TextField(10)