# HG changeset patch
# User wenzelm
# Date 1677695435 -3600
# Node ID ce53c1ce85368c0b0403b3589c397d4efe56a842
# Parent  5b9848b1ba30ff05fa9ea6007556f0ccddf9ee97
tuned signature;

diff -r 5b9848b1ba30 -r ce53c1ce8536 src/Pure/Tools/build_job.scala
--- 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)
 
diff -r 5b9848b1ba30 -r ce53c1ce8536 src/Pure/Tools/build_process.scala
--- 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
         }