1.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Nov 21 14:07:35 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Nov 21 12:11:21 2012 +0100
     1.3 @@ -39,11 +39,11 @@
     1.4    val group_tabs = new TabbedPane {
     1.5      pages ++= (for ((group, symbols) <- Symbol.groups) yield
     1.6        {
     1.7 -        new TabbedPane.Page(if (group == "") "Other" else group,
     1.8 +        new TabbedPane.Page(group,
     1.9            new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) },
    1.10 -          ("" /: (symbols take 10 map Symbol.decode))(_ + _ + " "))
    1.11 -      }).toList.sortWith(_.title.toUpperCase <= _.title.toUpperCase)
    1.12 -    pages += new TabbedPane.Page("Search", new BorderPanel {
    1.13 +          (symbols take 10 map Symbol.decode).mkString(" "))
    1.14 +      }).toList.sortWith(_.title <= _.title)
    1.15 +    pages += new TabbedPane.Page("search", new BorderPanel {
    1.16        val search = new TextField(10)
    1.17        val results_panel = new FlowPanel
    1.18        add(search, BorderPanel.Position.North)
    1.19 @@ -65,6 +65,7 @@
    1.20          }
    1.21        }
    1.22      }, "Search Symbols")
    1.23 +    pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") )
    1.24    }
    1.25    set_content(group_tabs)
    1.26  }