# HG changeset patch
# User immler
# Date 1353510240 -3600
# Node ID e6121a825db8866bbe4ee49c5a95e82c884ded06
# Parent  164af3238434d9dc883920f33a76cebd204d4ad8
delayed search to improve reactivity

diff -r 164af3238434 -r e6121a825db8 src/Tools/jEdit/src/symbols_dockable.scala
--- 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(" ") )
   }