# HG changeset patch
# User wenzelm
# Date 1708179638 -3600
# Node ID 389c1bfa7c3e87e96aaf2e7c23d7a742a0637556
# Parent  51e9d1a80e39387c762fd013ab6333e94e5de8fb
clarified signature: more standard defaults;

diff -r 51e9d1a80e39 -r 389c1bfa7c3e src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sat Feb 17 15:08:48 2024 +0100
+++ b/src/Pure/Build/build.scala	Sat Feb 17 15:20:38 2024 +0100
@@ -35,11 +35,11 @@
     hostname: String = Isabelle_System.hostname(),
     numa_shuffling: Boolean = false,
     build_heap: Boolean = false,
-    max_jobs: Option[Int] = None,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     session_setup: (String, Session) => Unit = (_, _) => (),
     build_uuid: String = UUID.random().toString,
+    jobs: Int = 0,
     master: Boolean = false
   ) {
     override def toString: String =
@@ -49,7 +49,6 @@
 
     def sessions_structure: isabelle.Sessions.Structure = deps.sessions_structure
 
-    def jobs: Int = max_jobs.getOrElse(1)
     def worker_active: Boolean = jobs > 0
   }
 
@@ -240,8 +239,9 @@
         val build_context =
           Context(store, build_deps, engine = build_engine, 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)
+            numa_shuffling = numa_shuffling, fresh_build = fresh_build,
+            no_build = no_build, session_setup = session_setup,
+            jobs = max_jobs.getOrElse(1), master = true)
 
         if (clean_build) {
           for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
@@ -625,7 +625,7 @@
         val build_context =
           Context(store, build_deps, engine = build_engine, afp_root = afp_root,
             hostname = hostname(build_options), numa_shuffling = numa_shuffling,
-            max_jobs = max_jobs, build_uuid = build_master.build_uuid)
+            build_uuid = build_master.build_uuid, jobs = max_jobs.getOrElse(1))
 
         build_engine.run_build_process(build_context, progress, server)
       }
diff -r 51e9d1a80e39 -r 389c1bfa7c3e src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Sat Feb 17 15:08:48 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Sat Feb 17 15:20:38 2024 +0100
@@ -45,8 +45,8 @@
         val selection = Sessions.Selection(sessions = List(benchmark_session))
         val full_sessions = Sessions.load_structure(options.int.update("threads", 1))
 
-        val build_context =
-          Build.Context(store, Sessions.deps(full_sessions.selection(selection)).check_errors)
+        val build_deps = Sessions.deps(full_sessions.selection(selection)).check_errors
+        val build_context = Build.Context(store, build_deps, jobs = 1)
 
         val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
         val session = sessions(benchmark_session)
diff -r 51e9d1a80e39 -r 389c1bfa7c3e src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Feb 17 15:08:48 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Feb 17 15:20:38 2024 +0100
@@ -1304,8 +1304,7 @@
       val build_context =
         Build.Context(store, build_deps, engine = Build_Engine, afp_root = afp_root,
           build_hosts = build_hosts, hostname = Build.hostname(build_options),
-          numa_shuffling = numa_shuffling, max_jobs = Some(0), session_setup = session_setup,
-          master = true)
+          numa_shuffling = numa_shuffling, session_setup = session_setup, master = true)
 
       val cluster_hosts = build_context.build_hosts