--- 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 =