# HG changeset patch # User immler # Date 1353496281 -3600 # Node ID 5f5e74365f14c3688785decc20de4d3dc0fea9b3 # Parent 8d2251b9a2003bcf7ad19cb3b5439247ba478382 capitalize lowercase groups; tuned with mkString diff -r 8d2251b9a200 -r 5f5e74365f14 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 14:07:35 2012 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 12:11:21 2012 +0100 @@ -39,11 +39,11 @@ val group_tabs = new TabbedPane { pages ++= (for ((group, symbols) <- Symbol.groups) yield { - new TabbedPane.Page(if (group == "") "Other" else group, + new TabbedPane.Page(group, new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) }, - ("" /: (symbols take 10 map Symbol.decode))(_ + _ + " ")) - }).toList.sortWith(_.title.toUpperCase <= _.title.toUpperCase) - pages += new TabbedPane.Page("Search", new BorderPanel { + (symbols take 10 map Symbol.decode).mkString(" ")) + }).toList.sortWith(_.title <= _.title) + pages += new TabbedPane.Page("search", new BorderPanel { val search = new TextField(10) val results_panel = new FlowPanel add(search, BorderPanel.Position.North) @@ -65,6 +65,7 @@ } } }, "Search Symbols") + pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") ) } set_content(group_tabs) }