tuned -- Symbol.groups already sorted;

--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 17:46:54 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 18:29:19 2012 +0100
@@ -56,14 +56,14 @@
   }
 
   val group_tabs: TabbedPane = new TabbedPane {
-    pages ++= (for ((group, symbols) <- Symbol.groups) yield
-      {
+    pages ++=
+      Symbol.groups map { case (group, symbols) =>
         new TabbedPane.Page(group,
           new FlowPanel {
             contents ++= symbols.map(new Symbol_Component(_))
             if (group == "control") contents += new Reset_Component
           }, null)
-      }).toList.sortWith(_.title <= _.title)
+      }
     pages += new TabbedPane.Page("search", new BorderPanel {
       val search = new TextField(10)
       val results_panel = new FlowPanel