more flexible Build.Engine.process_options: e.g. to manipulate "process_policy" for ML process;

--- a/src/Pure/System/host.scala	Sat Jul 22 13:31:55 2023 +0200
+++ b/src/Pure/System/host.scala	Sat Jul 22 16:01:46 2023 +0200
@@ -17,7 +17,7 @@
   def numactl(node: Int): String = "numactl -m" + node + " -N" + node
   def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok
 
-  def process_policy(options: Options, numa_node: Option[Int]): Options =
+  def process_policy_options(options: Options, numa_node: Option[Int]): Options =
     numa_node match {
       case None => options
       case Some(node) =>
@@ -32,9 +32,6 @@
   sealed case class Node_Info(hostname: String, numa_node: Option[Int]) {
     override def toString: String =
       hostname + if_proper(numa_node, "/" + numa_node.get.toString)
-
-    def process_policy(options: Options): Options =
-      Host.process_policy(options, numa_node)
   }
 
 

--- a/src/Pure/Tools/build.scala	Sat Jul 22 13:31:55 2023 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 22 16:01:46 2023 +0200
@@ -27,6 +27,7 @@
 
   sealed case class Context(
     store: Store,
+    engine: Engine,
     build_deps: isabelle.Sessions.Deps,
     afp_root: Option[Path] = None,
     build_hosts: List[Build_Cluster.Host] = Nil,
@@ -104,6 +105,9 @@
       else options1 + "build_database_server" + "build_database_test"
     }
 
+    def process_options(options: Options, node_info: Host.Node_Info): Options =
+      Host.process_policy_options(options, node_info.numa_node)
+
     final def build_store(options: Options,
       build_hosts: List[Build_Cluster.Host] = Nil,
       cache: Term.Cache = Term.Cache.make()
@@ -226,7 +230,7 @@
         /* build process and results */
 
         val build_context =
-          Context(store, build_deps, afp_root = afp_root, build_hosts = build_hosts,
+          Context(store, build_engine, build_deps, afp_root = afp_root, build_hosts = build_hosts,
             hostname = hostname(build_options), build_heap = build_heap,
             numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
             no_build = no_build, session_setup = session_setup, master = true)
@@ -523,7 +527,7 @@
             Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors
 
           val build_context =
-            Context(store, build_deps, afp_root = afp_root,
+            Context(store, build_engine, build_deps, afp_root = afp_root,
               hostname = hostname(build_options), numa_shuffling = numa_shuffling,
               max_jobs = max_jobs, build_uuid = build_master.build_uuid)
 

--- a/src/Pure/Tools/build_job.scala	Sat Jul 22 13:31:55 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Sat Jul 22 16:01:46 2023 +0200
@@ -114,7 +114,7 @@
     private val future_result: Future[(Process_Result, SHA1.Shasum)] =
       Future.thread("build", uninterruptible = true) {
         val info = session_background.sessions_structure(session_name)
-        val options = node_info.process_policy(info.options)
+        val options = build_context.engine.process_options(info.options, node_info)
 
         val store = build_context.store
 

--- a/src/Pure/Tools/dump.scala	Sat Jul 22 13:31:55 2023 +0200
+++ b/src/Pure/Tools/dump.scala	Sat Jul 22 16:01:46 2023 +0200
@@ -98,7 +98,7 @@
     ): Context = {
       val session_options: Options = {
         val options1 =
-          Host.process_policy(options, Host.numa_node0()) +
+          Host.process_policy_options(options, Host.numa_node0()) +
             "parallel_proofs=0" +
             "completion_limit=0" +
             "editor_tracing_messages=0"