clarified signature: move all parameters into Build_Process.Context;

--- a/src/Pure/Tools/build.scala	Mon Feb 20 11:38:21 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Feb 20 16:36:03 2023 +0100
@@ -127,7 +127,11 @@
 
     /* build process and results */
 
-    val build_context = Build_Process.Context(store, build_deps, progress = progress)
+    val build_context =
+      Build_Process.Context(store, build_deps, progress = progress,
+        build_heap = build_heap, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
+        fresh_build = fresh_build, no_build = no_build, verbose = verbose,
+        session_setup = session_setup)
 
     store.prepare_output_dir()
 
@@ -143,11 +147,9 @@
 
     val results =
       Isabelle_Thread.uninterruptible {
-        val build_process =
-          new Build_Process(build_context, build_heap = build_heap,
-            numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
-            no_build = no_build, verbose = verbose, session_setup = session_setup)
-        Results(build_context, build_process.run())
+        val build_process = new Build_Process(build_context)
+        val res = build_process.run()
+        Results(build_context, res)
       }
 
     if (export_files) {

--- a/src/Pure/Tools/build_process.scala	Mon Feb 20 11:38:21 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 20 16:36:03 2023 +0100
@@ -67,7 +67,14 @@
     def apply(
       store: Sessions.Store,
       deps: Sessions.Deps,
-      progress: Progress = new Progress
+      progress: Progress = new Progress,
+      build_heap: Boolean = false,
+      numa_shuffling: Boolean = false,
+      max_jobs: Int = 1,
+      fresh_build: Boolean = false,
+      no_build: Boolean = false,
+      verbose: Boolean = false,
+      session_setup: (String, Session) => Unit = (_, _) => ()
     ): Context = {
       val sessions_structure = deps.sessions_structure
       val build_graph = sessions_structure.build_graph
@@ -112,7 +119,9 @@
             }
         }
 
-      new Context(store, deps, sessions, ordering, progress)
+      new Context(store, deps, sessions, ordering, progress,
+        build_heap = build_heap, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
+        fresh_build = fresh_build, no_build = no_build, verbose = verbose, session_setup)
     }
   }
 
@@ -121,15 +130,22 @@
     val deps: Sessions.Deps,
     sessions: Map[String, Session_Context],
     val ordering: Ordering[String],
-    val progress: Progress
+    val progress: Progress,
+    val build_heap: Boolean,
+    val numa_shuffling: Boolean,
+    val max_jobs: Int,
+    val fresh_build: Boolean,
+    val no_build: Boolean,
+    val verbose: Boolean,
+    val session_setup: (String, Session) => Unit
   ) {
     def sessions_structure: Sessions.Structure = deps.sessions_structure
 
     def apply(session: String): Session_Context =
       sessions.getOrElse(session, Session_Context.empty(session, Time.zero))
 
-    def build_heap(session: String): Boolean =
-      Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session)
+    def do_store(session: String): Boolean =
+      build_heap || Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session)
   }
 
 
@@ -160,20 +176,12 @@
   }
 }
 
-class Build_Process(
-  build_context: Build_Process.Context,
-  build_heap: Boolean = false,
-  numa_shuffling: Boolean = false,
-  max_jobs: Int = 1,
-  fresh_build: Boolean = false,
-  no_build: Boolean = false,
-  verbose: Boolean = false,
-  session_setup: (String, Session) => Unit = (_, _) => ()
-) {
+class Build_Process(build_context: Build_Process.Context) {
   private val store = build_context.store
   private val build_options = store.options
   private val build_deps = build_context.deps
   private val progress = build_context.progress
+  private val verbose = build_context.verbose
 
   private val log =
     build_options.string("system_log") match {
@@ -183,7 +191,7 @@
     }
 
   // global state
-  private val _numa_nodes = new NUMA.Nodes(numa_shuffling)
+  private val _numa_nodes = new NUMA.Nodes(build_context.numa_shuffling)
   private var _pending: List[Build_Process.Entry] =
     (for ((name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator)
       yield Build_Process.Entry(name, preds.toList)).toList
@@ -197,7 +205,7 @@
   }
 
   private def next_pending(): Option[String] = synchronized {
-    if (_running.size < (max_jobs max 1)) {
+    if (_running.size < (build_context.max_jobs max 1)) {
       _pending.filter(entry => entry.is_ready && !_running.isDefinedAt(entry.name))
         .sortBy(_.name)(build_context.ordering)
         .headOption.map(_.name)
@@ -309,7 +317,7 @@
       }
       else SHA1.flat_shasum(ancestor_results.map(_.output_heap))
 
-    val do_store = build_heap || build_context.build_heap(session_name)
+    val do_store = build_context.do_store(session_name)
     val (current, output_heap) = {
       store.try_open_database(session_name) match {
         case Some(db) =>
@@ -317,7 +325,7 @@
             case Some(build) =>
               val output_heap = store.find_heap_shasum(session_name)
               val current =
-                !fresh_build &&
+                !build_context.fresh_build &&
                 build.ok &&
                 build.sources == build_deps.sources_shasum(session_name) &&
                 build.input_heaps == input_heaps &&
@@ -337,7 +345,7 @@
         add_result(session_name, true, output_heap, Process_Result.ok)
       }
     }
-    else if (no_build) {
+    else if (build_context.no_build) {
       progress.echo_if(verbose, "Skipping " + session_name + " ...")
       synchronized {
         remove_pending(session_name)
@@ -361,7 +369,7 @@
           val numa_node = next_numa_node()
           job_running(session_name,
             new Build_Job.Build_Session(progress, session_background, store, do_store,
-              resources, session_setup, input_heaps, numa_node))
+              resources, build_context.session_setup, input_heaps, numa_node))
         }
       job.start()
     }