# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1697652474 -7200
# Node ID eb572f7b668981a3083663e782810953efe046d8
# Parent  7f61688d4e8dd7f72faf69d06e579a65fdf21ee1
prefer extensible next_node_info in build process over process_options in build engine (which needs the final node info anyway);

diff -r 7f61688d4e8d -r eb572f7b6689 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Oct 18 19:53:39 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Oct 18 20:07:54 2023 +0200
@@ -114,9 +114,6 @@
       else options1 + "build_database_server" + "build_database"
     }
 
-    def process_options(options: Options, node_info: Host.Node_Info): Options =
-      Host.node_options(options, node_info)
-
     final def build_store(options: Options,
       build_hosts: List[Build_Cluster.Host] = Nil,
       cache: Term.Cache = Term.Cache.make()
diff -r 7f61688d4e8d -r eb572f7b6689 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Oct 18 19:53:39 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Wed Oct 18 20:07:54 2023 +0200
@@ -117,7 +117,7 @@
     private val future_result: Future[Option[Result]] =
       Future.thread("build", uninterruptible = true) {
         val info = session_background.sessions_structure(session_name)
-        val options = build_context.engine.process_options(info.options, node_info)
+        val options = Host.node_options(info.options, node_info)
 
         val store = build_context.store
 
diff -r 7f61688d4e8d -r eb572f7b6689 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Oct 18 19:53:39 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Oct 18 20:07:54 2023 +0200
@@ -984,6 +984,17 @@
     else Nil
   }
 
+  protected def next_node_info(state: Build_Process.State, session_name: String): Host.Node_Info = {
+    def used_nodes: Set[Int] =
+      Set.from(for (job <- state.running.valuesIterator; i <- job.node_info.numa_node) yield i)
+    val numa_node =
+      for {
+        db <- _host_database
+        n <- Host.next_numa_node(db, hostname, state.numa_nodes, used_nodes)
+      } yield n
+    Host.Node_Info(hostname, numa_node, Nil)
+  }
+
   protected def start_session(
     state: Build_Process.State,
     session_name: String,
@@ -1039,14 +1050,7 @@
       else state
     }
     else {
-      def used_nodes: Set[Int] =
-        Set.from(for (job <- state.running.valuesIterator; i <- job.node_info.numa_node) yield i)
-      val numa_node =
-        for {
-          db <- _host_database
-          n <- Host.next_numa_node(db, hostname, state.numa_nodes, used_nodes)
-        } yield n
-      val node_info = Host.Node_Info(hostname, numa_node, Nil)
+      val node_info = next_node_info(state, session_name)
 
       val print_node_info =
         node_info.numa_node.isDefined || node_info.rel_cpus.nonEmpty  ||