# HG changeset patch
# User wenzelm
# Date 1678278798 -3600
# Node ID 69d3547206db54375a433b8fd7d58bc2bb6903fe
# Parent  149d48a4801b330ea9ef6fb4182fee228ce7fe5c
clarified signature: prefer Build_Process.Context for parameters;

diff -r 149d48a4801b -r 69d3547206db src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 08 11:26:46 2023 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 08 13:33:18 2023 +0100
@@ -167,7 +167,7 @@
       Build_Process.Context(store, build_deps, progress = progress,
         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)
+        no_build = no_build, session_setup = session_setup, master = true)
 
     store.prepare_output()
     build_context.prepare_database()
@@ -186,7 +186,7 @@
       Isabelle_Thread.uninterruptible {
         val engine = get_engine(build_options.string("build_engine"))
         using(engine.init(build_context, progress)) { build_process =>
-          val res = build_process.run(master = true)
+          val res = build_process.run()
           Results(build_context, res)
         }
       }
diff -r 149d48a4801b -r 69d3547206db src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 08 11:26:46 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 08 13:33:18 2023 +0100
@@ -29,7 +29,8 @@
       fresh_build: Boolean = false,
       no_build: Boolean = false,
       session_setup: (String, Session) => Unit = (_, _) => (),
-      build_uuid: String = UUID.random().toString
+      build_uuid: String = UUID.random().toString,
+      master: Boolean = false,
     ): Context = {
       val sessions_structure = build_deps.sessions_structure
       val build_graph = sessions_structure.build_graph
@@ -83,7 +84,7 @@
       val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
       new Context(store, build_deps, sessions, ordering, ml_platform, hostname, numa_nodes,
         build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
-        no_build = no_build, session_setup, build_uuid = build_uuid)
+        no_build = no_build, session_setup, build_uuid = build_uuid, master = master)
     }
   }
 
@@ -100,7 +101,8 @@
     val fresh_build: Boolean,
     val no_build: Boolean,
     val session_setup: (String, Session) => Unit,
-    val build_uuid: String
+    val build_uuid: String,
+    val master: Boolean
   ) {
     override def toString: String =
       "Build_Process.Context(build_uuid = " + quote(build_uuid) + ")"
@@ -892,7 +894,7 @@
 
   /* run */
 
-  def run(master: Boolean = false): Map[String, Process_Result] = {
+  def run(): Map[String, Process_Result] = {
     def finished(): Boolean = synchronized_database { _state.finished }
 
     def sleep(): Unit =
@@ -917,7 +919,7 @@
       Map.empty[String, Process_Result]
     }
     else {
-      if (master) start_build()
+      if (build_context.master) start_build()
 
       val worker = build_context.worker
       if (worker) start_worker() else progress.echo("Waiting for external workers ...")
@@ -945,7 +947,7 @@
       }
       finally {
         if (worker) stop_worker()
-        if (master) stop_build()
+        if (build_context.master) stop_build()
       }
 
       synchronized_database {