src/Tools/jEdit/src/completion_popup.scala

--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -373,7 +373,7 @@
     }
 
     private val input_delay =
-      GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
+      Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
         action()
       }
 
@@ -530,7 +530,7 @@
     }
 
     private val process_delay =
-      GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
+      Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
         action()
       }