# HG changeset patch
# User wenzelm
# Date 1667764565 -3600
# Node ID 9600720071e6a4a6fbe23cdd4acfceebe712cc70
# Parent  5c7652e9bc01765f3451a39b4b7d8c3ae416de41
clarified delay -- more reactive;

diff -r 5c7652e9bc01 -r 9600720071e6 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Nov 06 20:44:12 2022 +0100
+++ b/src/Pure/Tools/build.scala	Sun Nov 06 20:56:05 2022 +0100
@@ -293,7 +293,9 @@
     }
 
     def sleep(): Unit =
-      Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep() }
+      Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
+        build_options.seconds("editor_input_delay").sleep()
+      }
 
     val log =
       build_options.string("system_log") match {