src/Tools/jEdit/src/symbols_dockable.scala
changeset 57612 990ffb84489b
parent 56769 8649243d7e91
child 57908 1937603dbdf2
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
@@ -70,7 +70,7 @@
         val search_space =
           (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
         val search_delay =
-          Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+          GUI_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
             val results =