src/Tools/jEdit/src/document_view.scala

--- a/src/Tools/jEdit/src/document_view.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -184,7 +184,7 @@
   /* caret handling */
 
   private val delay_caret_update =
-    GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+    Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
       session.caret_focus.post(Session.Caret_Focus)
       JEdit_Lib.invalidate(text_area)
     }