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