--- a/src/Pure/Tools/build_job.scala Wed Mar 01 19:18:03 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Wed Mar 01 19:30:35 2023 +0100
@@ -92,18 +92,19 @@
}
class Session_Job(
- progress: Progress,
- verbose: Boolean,
+ build_context: Build_Process.Context,
session_background: Sessions.Background,
session_heaps: List[Path],
- store: Sessions.Store,
do_store: Boolean,
resources: Resources,
- session_setup: (String, Session) => Unit,
sources_shasum: SHA1.Shasum,
input_heaps: SHA1.Shasum,
override val node_info: Node_Info
) extends Build_Job {
+ private val store = build_context.store
+ private val progress = build_context.progress
+ private val verbose = build_context.verbose
+
def session_name: String = session_background.session_name
def job_name: String = session_name
@@ -313,7 +314,7 @@
case _ =>
}
- session_setup(session_name, session)
+ build_context.session_setup(session_name, session)
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
--- a/src/Pure/Tools/build_process.scala Wed Mar 01 19:18:03 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Wed Mar 01 19:30:35 2023 +0100
@@ -628,9 +628,8 @@
val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
val job =
- new Build_Job.Session_Job(progress, verbose, session_background, session_heaps,
- store, do_store, resources, build_context.session_setup,
- build_deps.sources_shasum(session_name), input_heaps, node_info)
+ new Build_Job.Session_Job(build_context, session_background, session_heaps,
+ do_store, resources, build_deps.sources_shasum(session_name), input_heaps, node_info)
_state = state1.add_running(session_name, job)
job
}