# HG changeset patch
# User wenzelm
# Date 1353778159 -3600
# Node ID 22d0f64362a50a5d9b50101c15b4f4737faa8f6b
# Parent  8b5a256859af5a474090bd31473b6fe61d8f0a21
tuned -- Symbol.groups already sorted;

diff -r 8b5a256859af -r 22d0f64362a5 src/Tools/jEdit/src/symbols_dockable.scala
--- 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