--- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 14:53:26 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 16:04:00 2012 +0100
@@ -36,7 +36,7 @@
tooltip = symbol + " - " + get_name(dec)
}
- val group_tabs = new TabbedPane {
+ val group_tabs: TabbedPane = new TabbedPane {
pages ++= (for ((group, symbols) <- Symbol.groups) yield
{
new TabbedPane.Page(group,
@@ -49,10 +49,8 @@
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,10 +58,10 @@
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(" ") )
}