# HG changeset patch
# User wenzelm
# Date 1677759561 -3600
# Node ID 362bf802013ec67c4a2bf0dfe175a28a813ad4f3
# Parent  a073ac3f3b563a32b6f835c9f33f369ef3de6b56
clarified modules;

diff -r a073ac3f3b56 -r 362bf802013e src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Mar 02 11:36:10 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Mar 02 13:19:21 2023 +0100
@@ -97,9 +97,6 @@
   class Session_Job(
     build_context: Build_Process.Context,
     session_background: Sessions.Background,
-    session_heaps: List[Path],
-    store_heap: Boolean,
-    resources: Resources,
     input_shasum: SHA1.Shasum,
     override val node_info: Node_Info
   ) extends Build_Job {
@@ -116,12 +113,20 @@
     val session_sources: Sessions.Sources =
       Sessions.Sources.load(session_background.base, cache = store.cache.compress)
 
+    val store_heap = build_context.store_heap(session_name)
+
     private val future_result: Future[Process_Result] =
       Future.thread("build", uninterruptible = true) {
         val env =
           Isabelle_System.settings(
             List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString))
 
+        val session_heaps =
+          session_background.info.parent match {
+            case None => Nil
+            case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic)
+          }
+
         val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil
 
         val eval_store =
@@ -152,6 +157,10 @@
                 }
           }
 
+        val resources =
+          new Resources(session_background, log = build_context.log,
+            command_timings = build_context.old_command_timings(session_name))
+
         val session =
           new Session(options, resources) {
             override val cache: Term.Cache = store.cache
diff -r a073ac3f3b56 -r 362bf802013e src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Mar 02 11:36:10 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 02 13:19:21 2023 +0100
@@ -598,22 +598,11 @@
 
       store.init_output(session_name)
 
-      val session_background = build_deps.background(session_name)
-      val session_heaps =
-        session_background.info.parent match {
-          case None => Nil
-          case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic)
-        }
-
-      val resources =
-        new Resources(session_background, log = build_context.log,
-          command_timings = build_context.old_command_timings(session_name))
-
       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(build_context, session_background, session_heaps,
-          store_heap, resources, input_shasum, node_info)
+        new Build_Job.Session_Job(
+          build_context, build_deps.background(session_name), input_shasum, node_info)
       state1.add_running(session_name, job)
     }
   }