# HG changeset patch
# User wenzelm
# Date 1709585181 -3600
# Node ID 5bcb1b368b3054603be08cbebc54bcde0698d17d
# Parent  e9e74577755f32ee69590e225510abe38e42cbc8
clarified module signature and state;

diff -r e9e74577755f -r 5bcb1b368b30 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Mon Mar 04 21:22:22 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Mon Mar 04 21:46:21 2024 +0100
@@ -1126,24 +1126,24 @@
 
   /* run */
 
-  protected def finished_unsynchronized(): Boolean =
+  def finished(): Boolean = synchronized {
     if (!build_context.master && progress.stopped) _state.build_running.isEmpty
     else _state.pending.isEmpty
+  }
 
   protected def sleep(): Unit =
     Isabelle_Thread.interrupt_handler(_ => progress.stop()) { build_delay.sleep() }
 
   def run(): Build.Results = {
-    var finished = false
-
-    synchronized_database("Build_Process.init") {
-      if (build_context.master) {
-        _build_cluster.init()
-        _state = init_state(_state)
+    val vacuous =
+      synchronized_database("Build_Process.init") {
+        if (build_context.master) {
+          _build_cluster.init()
+          _state = init_state(_state)
+        }
+        _state = _state.copy(numa_nodes = Host.numa_nodes(enabled = build_context.numa_shuffling))
+        build_context.master && _state.pending.isEmpty
       }
-      _state = _state.copy(numa_nodes = Host.numa_nodes(enabled = build_context.numa_shuffling))
-      finished = finished_unsynchronized()
-    }
 
     def check_jobs_unsynchronized(): Boolean = {
       val jobs = next_jobs(_state)
@@ -1162,7 +1162,7 @@
       jobs.nonEmpty
     }
 
-    if (finished) {
+    if (vacuous) {
       progress.echo_warning("Nothing to build")
       Build.Results(build_context)
     }
@@ -1172,7 +1172,7 @@
       _build_cluster.start()
 
       try {
-        while (!finished) {
+        while (!finished()) {
           val check_jobs =
             synchronized_database("Build_Process.main") {
               if (progress.stopped) _state.stop_running()
@@ -1193,7 +1193,6 @@
                 }
               }
 
-              finished = finished_unsynchronized()
               check_jobs_unsynchronized()
             }