# 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)
 }