# HG changeset patch
# User wenzelm
# Date 1709585933 -3600
# Node ID 48af00f6f110c325a681a2839464a9f7793569f5
# Parent  5bcb1b368b3054603be08cbebc54bcde0698d17d
clarified signature;
sleep unconditionally: avoid aggressive database access;

diff -r 5bcb1b368b30 -r 48af00f6f110 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Mon Mar 04 21:46:21 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Mon Mar 04 21:58:53 2024 +0100
@@ -1126,7 +1126,7 @@
 
   /* run */
 
-  def finished(): Boolean = synchronized {
+  protected def finished(): Boolean = synchronized {
     if (!build_context.master && progress.stopped) _state.build_running.isEmpty
     else _state.pending.isEmpty
   }
@@ -1134,6 +1134,37 @@
   protected def sleep(): Unit =
     Isabelle_Thread.interrupt_handler(_ => progress.stop()) { build_delay.sleep() }
 
+  protected def main_unsynchronized(): Unit = {
+    for (job <- _state.finished_running()) {
+      job.join_build match {
+        case None =>
+          _state = _state.remove_running(job.name)
+        case Some(result) =>
+          val result_name = (job.name, worker_uuid, build_uuid)
+          _state = _state.
+            remove_pending(job.name).
+            remove_running(job.name).
+            make_result(result_name,
+              result.process_result,
+              result.output_shasum,
+              node_info = job.node_info)
+      }
+    }
+
+    for (name <- next_jobs(_state)) {
+      if (is_session_name(name)) {
+        if (build_context.sessions_structure.defined(name)) {
+          _state.ancestor_results(name) match {
+            case Some(results) => _state = start_session(_state, name, results)
+            case None => warning("Bad build job " + quote(name) + ": no ancestor results")
+          }
+        }
+        else warning("Bad build job " + quote(name) + ": no session info")
+      }
+      else warning("Bad build job " + quote(name))
+    }
+  }
+
   def run(): Build.Results = {
     val vacuous =
       synchronized_database("Build_Process.init") {
@@ -1144,24 +1175,6 @@
         _state = _state.copy(numa_nodes = Host.numa_nodes(enabled = build_context.numa_shuffling))
         build_context.master && _state.pending.isEmpty
       }
-
-    def check_jobs_unsynchronized(): Boolean = {
-      val jobs = next_jobs(_state)
-      for (name <- jobs) {
-        if (is_session_name(name)) {
-          if (build_context.sessions_structure.defined(name)) {
-            _state.ancestor_results(name) match {
-              case Some(results) => _state = start_session(_state, name, results)
-              case None => warning("Bad build job " + quote(name) + ": no ancestor results")
-            }
-          }
-          else warning("Bad build job " + quote(name) + ": no session info")
-        }
-        else warning("Bad build job " + quote(name))
-      }
-      jobs.nonEmpty
-    }
-
     if (vacuous) {
       progress.echo_warning("Nothing to build")
       Build.Results(build_context)
@@ -1173,30 +1186,11 @@
 
       try {
         while (!finished()) {
-          val check_jobs =
-            synchronized_database("Build_Process.main") {
-              if (progress.stopped) _state.stop_running()
-
-              for (job <- _state.finished_running()) {
-                job.join_build match {
-                  case None =>
-                    _state = _state.remove_running(job.name)
-                  case Some(result) =>
-                    val result_name = (job.name, worker_uuid, build_uuid)
-                    _state = _state.
-                      remove_pending(job.name).
-                      remove_running(job.name).
-                      make_result(result_name,
-                        result.process_result,
-                        result.output_shasum,
-                        node_info = job.node_info)
-                }
-              }
-
-              check_jobs_unsynchronized()
-            }
-
-          if (!check_jobs) sleep()
+          synchronized_database("Build_Process.main") {
+            if (progress.stopped) _state.stop_running()
+            main_unsynchronized()
+          }
+          sleep()
         }
       }
       finally {