# HG changeset patch
# User wenzelm
# Date 1586170425 -7200
# Node ID b9a5eb0f3b43c51f8dc814f6437fffad6c085183
# Parent  8ec5c82b67dcf80cf7130b2080492b13713431fc
clarified modules;

diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Pure/Concurrent/delay.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/delay.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -0,0 +1,66 @@
+/*  Title:      Pure/Concurrent/delay.scala
+    Author:     Makarius
+
+Delayed events.
+*/
+
+package isabelle
+
+
+object Delay
+{
+  // delayed event after first invocation
+  def first(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+    new Delay(true, delay, log, if (gui) GUI_Thread.later { event } else event )
+
+  // delayed event after last invocation
+  def last(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+    new Delay(false, delay, log, if (gui) GUI_Thread.later { event } else event )
+}
+
+final class Delay private(first: Boolean, delay: => Time, log: Logger, event: => Unit)
+{
+  private var running: Option[Event_Timer.Request] = None
+
+  private def run: Unit =
+  {
+    val do_run = synchronized {
+      if (running.isDefined) { running = None; true } else false
+    }
+    if (do_run) {
+      try { event }
+      catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
+    }
+  }
+
+  def invoke(): Unit = synchronized
+  {
+    val new_run =
+      running match {
+        case Some(request) => if (first) false else { request.cancel; true }
+        case None => true
+      }
+    if (new_run)
+      running = Some(Event_Timer.request(Time.now() + delay)(run))
+  }
+
+  def revoke(): Unit = synchronized
+  {
+    running match {
+      case Some(request) => request.cancel; running = None
+      case None =>
+    }
+  }
+
+  def postpone(alt_delay: Time): Unit = synchronized
+  {
+    running match {
+      case Some(request) =>
+        val alt_time = Time.now() + alt_delay
+        if (request.time < alt_time && request.cancel) {
+          running = Some(Event_Timer.request(alt_time)(run))
+        }
+      case None =>
+    }
+  }
+}
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -95,65 +95,6 @@
 
   def uninterruptible[A](body: => A): A =
     interrupt_handler(Interrupt_Handler.uninterruptible)(body)
-
-
-  /* delayed events */
-
-  final class Delay private[Isabelle_Thread](
-    first: Boolean, delay: => Time, log: Logger, event: => Unit)
-  {
-    private var running: Option[Event_Timer.Request] = None
-
-    private def run: Unit =
-    {
-      val do_run = synchronized {
-        if (running.isDefined) { running = None; true } else false
-      }
-      if (do_run) {
-        try { event }
-        catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
-      }
-    }
-
-    def invoke(): Unit = synchronized
-    {
-      val new_run =
-        running match {
-          case Some(request) => if (first) false else { request.cancel; true }
-          case None => true
-        }
-      if (new_run)
-        running = Some(Event_Timer.request(Time.now() + delay)(run))
-    }
-
-    def revoke(): Unit = synchronized
-    {
-      running match {
-        case Some(request) => request.cancel; running = None
-        case None =>
-      }
-    }
-
-    def postpone(alt_delay: Time): Unit = synchronized
-    {
-      running match {
-        case Some(request) =>
-          val alt_time = Time.now() + alt_delay
-          if (request.time < alt_time && request.cancel) {
-            running = Some(Event_Timer.request(alt_time)(run))
-          }
-        case None =>
-      }
-    }
-  }
-
-  // delayed event after first invocation
-  def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
-    new Delay(true, delay, log, event)
-
-  // delayed event after last invocation
-  def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
-    new Delay(false, delay, log, event)
 }
 
 class Isabelle_Thread private(
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/GUI/gui_thread.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -54,13 +54,4 @@
       promise
     }
   }
-
-
-  /* delayed events */
-
-  def delay_first(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
-    Isabelle_Thread.delay_first(delay) { later { event } }
-
-  def delay_last(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
-    Isabelle_Thread.delay_last(delay) { later { event } }
 }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/General/file_watcher.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -84,7 +84,7 @@
 
     /* changed directory entries */
 
-    private val delay_changed = Isabelle_Thread.delay_last(delay)
+    private val delay_changed = Delay.last(delay)
     {
       val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
       handle(changed)
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -304,12 +304,12 @@
       val consumer =
       {
         val delay_nodes_status =
-          Isabelle_Thread.delay_first(nodes_status_delay max Time.zero) {
+          Delay.first(nodes_status_delay max Time.zero) {
             progress.nodes_status(use_theories_state.value.nodes_status)
           }
 
         val delay_commit_clean =
-          Isabelle_Thread.delay_first(commit_cleanup_delay max Time.zero) {
+          Delay.first(commit_cleanup_delay max Time.zero) {
             val clean_theories = use_theories_state.change_result(_.clean_theories)
             if (clean_theories.nonEmpty) {
               progress.echo("Removing " + clean_theories.length + " theories ...")
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -268,7 +268,7 @@
       nodes = Set.empty
       commands = Set.empty
     }
-    private val delay_flush = Isabelle_Thread.delay_first(output_delay) { flush() }
+    private val delay_flush = Delay.first(output_delay) { flush() }
 
     def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
       synchronized {
@@ -313,7 +313,7 @@
   private object consolidation
   {
     private val delay =
-      Isabelle_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
+      Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) }
 
     private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
     private val state = Synchronized(init_state)
@@ -382,7 +382,7 @@
   /* manager thread */
 
   private val delay_prune =
-    Isabelle_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
+    Delay.first(prune_delay) { manager.send(Prune_History) }
 
   private val manager: Consumer_Thread[Any] =
   {
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -155,7 +155,7 @@
   private val state = Synchronized(Debugger.State())
 
   private val delay_update =
-    Isabelle_Thread.delay_first(session.output_delay) {
+    Delay.first(session.output_delay) {
       session.debugger_updates.post(Debugger.Update)
     }
 
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/build-jars	Mon Apr 06 12:53:45 2020 +0200
@@ -28,6 +28,7 @@
   src/Pure/Admin/other_isabelle.scala
   src/Pure/Concurrent/consumer_thread.scala
   src/Pure/Concurrent/counter.scala
+  src/Pure/Concurrent/delay.scala
   src/Pure/Concurrent/event_timer.scala
   src/Pure/Concurrent/future.scala
   src/Pure/Concurrent/isabelle_thread.scala
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/Graphview/tree_panel.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -112,7 +112,7 @@
   private val selection_field_foreground = selection_field.foreground
 
   private val selection_delay =
-    GUI_Thread.delay_last(graphview.options.seconds("editor_input_delay")) {
+    Delay.last(graphview.options.seconds("editor_input_delay"), gui = true) {
       val (pattern, ok) =
         selection_field.text match {
           case null | "" => (None, true)
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/VSCode/src/server.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -127,12 +127,12 @@
 
   /* input from client or file-system */
 
-  private val delay_input: Isabelle_Thread.Delay =
-    Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+  private val delay_input: Delay =
+    Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
     { resources.flush_input(session, channel) }
 
-  private val delay_load: Isabelle_Thread.Delay =
-    Isabelle_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
+  private val delay_load: Delay =
+    Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
       val (invoke_input, invoke_load) =
         resources.resolve_dependencies(session, editor, file_watcher)
       if (invoke_input) delay_input.invoke()
@@ -183,8 +183,8 @@
 
   /* caret handling */
 
-  private val delay_caret_update: Isabelle_Thread.Delay =
-    Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+  private val delay_caret_update: Delay =
+    Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
     { session.caret_focus.post(Session.Caret_Focus) }
 
   private def update_caret(caret: Option[(JFile, Line.Position)])
@@ -199,8 +199,8 @@
 
   private lazy val preview_panel = new Preview_Panel(resources)
 
-  private lazy val delay_preview: Isabelle_Thread.Delay =
-    Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+  private lazy val delay_preview: Delay =
+    Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger)
     {
       if (preview_panel.flush(channel)) delay_preview.invoke()
     }
@@ -214,8 +214,8 @@
 
   /* output to client */
 
-  private val delay_output: Isabelle_Thread.Delay =
-    Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+  private val delay_output: Delay =
+    Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger)
     {
       if (resources.flush_output(channel)) delay_output.invoke()
     }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 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()
       }
 
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -362,7 +362,7 @@
   /* resize */
 
   private val delay_resize =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 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)
     }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/font_info.scala
--- a/src/Tools/jEdit/src/font_info.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/font_info.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -56,7 +56,7 @@
 
     // owned by GUI thread
     private var steps = 0
-    private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+    private val delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true)
     {
       change_size(size =>
         {
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -80,7 +80,7 @@
   /* resize */
 
   private val delay_resize =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -32,10 +32,10 @@
   def purge() { flush_edits(purge = true) }
 
   private val delay1_flush =
-    GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
+    Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() }
 
   private val delay2_flush =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() }
+    Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() }
 
   def invoke(): Unit = delay1_flush.invoke()
   def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -59,10 +59,10 @@
     }
 
   private val input_delay =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_input_delay")) { update_chart }
+    Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart }
 
   private val update_delay =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
+    Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart }
 
 
   /* controls */
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -151,7 +151,7 @@
   /* resize */
 
   private val delay_resize =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -107,7 +107,7 @@
   /* theory files */
 
   lazy val delay_init =
-    GUI_Thread.delay_last(options.seconds("editor_load_delay"))
+    Delay.last(options.seconds("editor_load_delay"), gui = true)
     {
       init_models()
     }
@@ -178,7 +178,7 @@
   }
 
   private lazy val delay_load =
-    GUI_Thread.delay_last(options.seconds("editor_load_delay")) { delay_load_action() }
+    Delay.last(options.seconds("editor_load_delay"), gui = true) { delay_load_action() }
 
   private def file_watcher_action(changed: Set[JFile]): Unit =
     if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -191,7 +191,7 @@
     Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
       {
         private val input_delay =
-          GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+          Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
             search_action(this)
           }
         getDocument.addDocumentListener(new DocumentListener {
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -77,7 +77,7 @@
   private var active = true
 
   private val pending_delay =
-    GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+    Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
       pending match {
         case Some(body) => pending = None; body()
         case None =>
@@ -99,7 +99,7 @@
     }
 
   private lazy val reactivate_delay =
-    GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+    Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
       active = true
     }
 
@@ -113,7 +113,7 @@
 
   /* dismiss */
 
-  private lazy val focus_delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+  private lazy val focus_delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true)
   {
     dismiss_unfocused()
   }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -320,7 +320,7 @@
     }
 
   private val delay_resize =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -102,7 +102,7 @@
       }
 
     private val delay_exit =
-      GUI_Thread.delay_first(Time.seconds(1.0))
+      Delay.first(Time.seconds(1.0), gui = true)
       {
         if (can_auto_close) conclude()
         else {
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -144,7 +144,7 @@
   /* resize */
 
   private val delay_resize =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -182,7 +182,7 @@
   /* resize */
 
   private val delay_resize =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   peer.addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -58,7 +58,7 @@
   /* resize */
 
   private val delay_resize =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -40,7 +40,7 @@
   /* resize */
 
   private val delay_resize =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -28,7 +28,7 @@
   private val abbrevs_panel = new Abbrevs_Panel
 
   private val abbrevs_refresh_delay =
-    GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
+    Delay.last(PIDE.options.seconds("editor_update_delay"), gui = true) { abbrevs_panel.refresh }
 
   private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
   {
@@ -129,7 +129,7 @@
 
     val search_space = for ((sym, _) <- Symbol.codes) yield (sym, Word.lowercase(sym))
     val search_delay =
-      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+      Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
         val search_words = Word.explode(Word.lowercase(search_field.text))
         val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
         val results =
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/syslog_dockable.scala
--- a/src/Tools/jEdit/src/syslog_dockable.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -21,7 +21,7 @@
 
   private val syslog = new TextArea()
 
-  private def syslog_delay = GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
+  private def syslog_delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true)
   {
     val text = PIDE.session.syslog_content()
     if (text != syslog.text) syslog.text = text
diff -r 8ec5c82b67dc -r b9a5eb0f3b43 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -75,7 +75,7 @@
   private var current_overview = Overview()
 
   private val delay_repaint =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { repaint() }
 
   override def paintComponent(gfx: Graphics)
   {
@@ -116,7 +116,7 @@
   def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
 
   private val delay_refresh =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) {
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
       if (!doc_view.rich_text_area.check_robust_body) invoke()
       else {
         JEdit_Lib.buffer_lock(buffer) {