src/Pure/Tools/build_process.scala
changeset 78406 2ece6509ad6f
parent 78401 822ddccda899
child 78409 f2d67c78b689
--- 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)