clarified options;
authorwenzelm
Sun, 16 Jul 2023 14:11:56 +0200
changeset 78364 e33cca11b474
parent 78363 fca9ec5a615c
child 78365 bb5e2a7198e3
clarified options;
etc/options
src/Pure/Tools/build_process.scala
--- a/etc/options	Sun Jul 16 13:45:46 2023 +0200
+++ b/etc/options	Sun Jul 16 14:11:56 2023 +0200
@@ -198,6 +198,9 @@
 option build_database_slice : real = 300
   -- "slice size in MiB for ML heap stored within database"
 
+option build_delay : real = 0.2
+  -- "delay build process main loop"
+
 
 section "Editor Session"
 
--- a/src/Pure/Tools/build_process.scala	Sun Jul 16 13:45:46 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Jul 16 14:11:56 2023 +0200
@@ -1071,7 +1071,7 @@
 
     def sleep(): Unit =
       Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
-        build_options.seconds("editor_input_delay").sleep()
+        build_options.seconds("build_delay").sleep()
       }
 
     def start_job(): Boolean = synchronized_database("Build_Process.start_job") {