--- 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") {