src/Pure/Build/build_process.scala

   }
 
 
   /* 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)
-      }
-      _state = _state.copy(numa_nodes = Host.numa_nodes(enabled = build_context.numa_shuffling))
-      finished = finished_unsynchronized()
-    }
+    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
+      }
 
     def check_jobs_unsynchronized(): Boolean = {
       val jobs = next_jobs(_state)
       for (name <- jobs) {
         if (is_session_name(name)) {

         else warning("Bad build job " + quote(name))
       }
       jobs.nonEmpty
     }
 
-    if (finished) {
+    if (vacuous) {
       progress.echo_warning("Nothing to build")
       Build.Results(build_context)
     }
     else {
       if (build_context.master) start_build()
       start_worker()
       _build_cluster.start()
 
       try {
-        while (!finished) {
+        while (!finished()) {
           val check_jobs =
             synchronized_database("Build_Process.main") {
               if (progress.stopped) _state.stop_running()
 
               for (job <- _state.finished_running()) {

                         result.output_shasum,
                         node_info = job.node_info)
                 }
               }
 
-              finished = finished_unsynchronized()
               check_jobs_unsynchronized()
             }
 
           if (!check_jobs) sleep()
         }