clarified options: accommodate potentially slow database connection;

--- a/etc/options	Wed Jul 19 13:17:38 2023 +0200
+++ b/etc/options	Wed Jul 19 13:29:18 2023 +0200
@@ -201,9 +201,12 @@
 option build_database_slice : real = 300
   -- "slice size in MiB for ML heap stored within database"
 
-option build_delay : real = 0.5
+option build_delay : real = 0.2
   -- "delay build process main loop"
 
+option build_database_delay : real = 1.0
+  -- "delay build process main loop (via central database)"
+
 
 section "Editor Session"
 

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