# HG changeset patch
# User wenzelm
# Date 1398687554 -7200
# Node ID 8649243d7e91a30c7177579eb99ec40d6fcde6ec
# Parent  06388a5cfb7c493641e57e2e969bf899f4875fc2
tuned;

diff -r 06388a5cfb7c -r 8649243d7e91 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Mon Apr 28 12:56:54 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Mon Apr 28 14:19:14 2014 +0200
@@ -69,7 +69,7 @@
   
         val search_space =
           (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
-        val delay_search =
+        val search_delay =
           Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
             val search_words = Word.explode(Word.lowercase(search_field.text))
             val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
@@ -85,7 +85,7 @@
             revalidate
             repaint
           }
-          search_field.reactions += { case ValueChanged(_) => delay_search.invoke() }
+          search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
       }, "Search Symbols")
     pages += search_page