diff -r 8ff1698e7247 -r 2ece6509ad6f src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Wed Jul 19 13:17:38 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Wed Jul 19 13:29:18 2023 +0200 @@ -879,6 +879,9 @@ } catch { case exn: Throwable => close(); throw exn } + protected val build_delay: Time = + build_options.seconds(if (_build_database.isEmpty) "build_delay" else "build_database_delay") + private val _host_database: Option[SQL.Database] = try { store.maybe_open_build_database(path = Host.private_data.database, server = server) } catch { case exn: Throwable => close(); throw exn } @@ -1082,9 +1085,7 @@ def finished(): Boolean = synchronized_database("Build_Process.test") { _state.finished } def sleep(): Unit = - Isabelle_Thread.interrupt_handler(_ => progress.stop()) { - build_options.seconds("build_delay").sleep() - } + Isabelle_Thread.interrupt_handler(_ => progress.stop()) { build_delay.sleep() } def check_jobs(): Boolean = synchronized_database("Build_Process.check_jobs") { val jobs = next_jobs(_state)