# HG changeset patch
# User wenzelm
# Date 1710073935 -3600
# Node ID dc517696e5ffb3a884d7ae127b19c7dce81ee557
# Parent  f7dfe92e67857bd759d3ca1283b96df3ddedd590
clarified signature: init_state vs. init_unsynchronized;

diff -r f7dfe92e6785 -r dc517696e5ff src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Sun Mar 10 12:03:46 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Sun Mar 10 13:32:15 2024 +0100
@@ -1042,17 +1042,6 @@
 
   /* policy operations */
 
-  protected def init_state(state: Build_Process.State): Build_Process.State = {
-    val sessions1 = state.sessions.init(build_context, _database_server, progress = build_progress)
-    val pending1 =
-      sessions1.iterator.foldLeft(state.pending) {
-        case (map, session) =>
-          if (map.isDefinedAt(session.name)) map
-          else map + Build_Process.Task.entry(session, build_context)
-      }
-    state.copy(sessions = sessions1, pending = pending1)
-  }
-
   protected def next_jobs(state: Build_Process.State): List[String] = {
     val limit = {
       if (progress.stopped) { if (build_context.master) Int.MaxValue else 0 }
@@ -1210,6 +1199,24 @@
   protected def sleep(): Unit =
     Isabelle_Thread.interrupt_handler(_ => progress.stop()) { build_delay.sleep() }
 
+  protected def init_unsynchronized(): Unit = {
+    if (build_context.master) {
+      val sessions1 =
+        _state.sessions.init(build_context, _database_server, progress = build_progress)
+      val pending1 =
+        sessions1.iterator.foldLeft(_state.pending) {
+          case (map, session) =>
+            if (map.isDefinedAt(session.name)) map
+            else map + Build_Process.Task.entry(session, build_context)
+        }
+      _state = _state.copy(sessions = sessions1, pending = pending1)
+    }
+
+    val numa_nodes = Host.numa_nodes(enabled = build_context.numa_shuffling)
+    _state = _state.copy(numa_nodes = numa_nodes)
+  }
+
+
   protected def main_unsynchronized(): Unit = {
     for (job <- _state.build_running.filter(_.is_finished)) {
       _state = _state.remove_running(job.name)
@@ -1241,11 +1248,8 @@
   def run(): Build.Results = {
     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))
+        if (build_context.master) _build_cluster.init()
+        init_unsynchronized()
         build_context.master && _state.pending.isEmpty
       }
     if (vacuous) {