# HG changeset patch
# User wenzelm
# Date 1708177712 -3600
# Node ID 8b8591820bd819d01a60787e3bd1b1f4bca0e594
# Parent  7eaf1931f408b2f92dc3cb75e87d5b5f46f6a65e
clarified signature: prefer default;

diff -r 7eaf1931f408 -r 8b8591820bd8 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Feb 16 20:54:21 2024 +0100
+++ b/src/Pure/Build/build.scala	Sat Feb 17 14:48:32 2024 +0100
@@ -27,8 +27,8 @@
 
   sealed case class Context(
     store: Store,
-    engine: Engine,
     build_deps: isabelle.Sessions.Deps,
+    engine: Engine = Default_Engine,
     afp_root: Option[Path] = None,
     build_hosts: List[Build_Cluster.Host] = Nil,
     ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
@@ -237,8 +237,8 @@
         /* build process and results */
 
         val build_context =
-          Context(store, build_engine, build_deps, afp_root = afp_root, build_hosts = build_hosts,
-            hostname = hostname(build_options), build_heap = build_heap,
+          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)
 
@@ -622,7 +622,7 @@
           Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors
 
         val build_context =
-          Context(store, build_engine, build_deps, afp_root = afp_root,
+          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)
 
diff -r 7eaf1931f408 -r 8b8591820bd8 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Fri Feb 16 20:54:21 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Sat Feb 17 14:48:32 2024 +0100
@@ -46,8 +46,7 @@
         val full_sessions = Sessions.load_structure(options.int.update("threads", 1))
 
         val build_context =
-          Build.Context(store, Build.Default_Engine,
-            Sessions.deps(full_sessions.selection(selection)).check_errors)
+          Build.Context(store, Sessions.deps(full_sessions.selection(selection)).check_errors)
 
         val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
         val session = sessions(benchmark_session)
diff -r 7eaf1931f408 -r 8b8591820bd8 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Fri Feb 16 20:54:21 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Feb 17 14:48:32 2024 +0100
@@ -1304,7 +1304,7 @@
           inlined_files = true).check_errors
 
       val build_context =
-        Build.Context(store, build_engine, build_deps, afp_root = afp_root,
+        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)