clarified delay -- more reactive;
authorwenzelm
Sun, 06 Nov 2022 20:56:05 +0100
changeset 76476 9600720071e6
parent 76475 5c7652e9bc01
child 76477 6e68ec0fdc48
clarified delay -- more reactive;
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 {