merged

--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Nov 21 15:52:44 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Nov 21 16:43:14 2012 +0100
@@ -30,29 +30,28 @@
   {
     val dec = Symbol.decode(symbol)
     font =
-      new Font(Isabelle.font_family(),
+      new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
         Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
     action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
-    tooltip = symbol + " - " + get_name(dec)
+    tooltip = symbol +
+      (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "") +
+      " - " + get_name(dec)
   }
 
-  val group_tabs = new TabbedPane {
+  val group_tabs: TabbedPane = new TabbedPane {
     pages ++= (for ((group, symbols) <- Symbol.groups) yield
       {
-        new TabbedPane.Page(if (group == "") "Other" else 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 {
+        new TabbedPane.Page(group,
+          new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) })
+      }).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)
       add(results_panel, BorderPanel.Position.Center)
       listenTo(search)
-      var last = search.text
-      reactions += { case ValueChanged(`search`) =>
-        if (search.text != last) {
-          last = search.text
+      val delay_search =
+        Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
           results_panel.contents.clear
           val results =
             (searchspace filter (search.text.toLowerCase.split("\\s+") forall _._2.contains)
@@ -60,11 +59,12 @@
           for ((sym, _) <- results)
             results_panel.contents += new Symbol_Component(sym)
           if (results.length > max_results) results_panel.contents += new Label("...")
-          results_panel.revalidate
-          results_panel.repaint
+          revalidate
+          repaint
         }
-      }
+      reactions += { case ValueChanged(`search`) => delay_search.invoke() }
     }, "Search Symbols")
+    pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") )
   }
   set_content(group_tabs)
 }