# HG changeset patch
# User wenzelm
# Date 1671300400 -3600
# Node ID dd03c91cda430e34d74e678ab9d9e125248d51bd
# Parent  fa81f218c96e793cd93102a3d1d3ab0e3356fd3b
clarified signature;

diff -r fa81f218c96e -r dd03c91cda43 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Dec 17 17:28:05 2022 +0100
+++ b/src/Pure/Tools/build.scala	Sat Dec 17 19:06:40 2022 +0100
@@ -428,7 +428,7 @@
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
-                    new Build_Job(progress, session_name, info, build_deps, store, do_store,
+                    new Build_Job(progress, build_deps.background(session_name), store, do_store,
                       log, session_setup, numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
diff -r fa81f218c96e -r dd03c91cda43 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Dec 17 17:28:05 2022 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Dec 17 19:06:40 2022 +0100
@@ -237,9 +237,7 @@
 }
 
 class Build_Job(progress: Progress,
-  session_name: String,
-  val info: Sessions.Info,
-  deps: Sessions.Deps,
+  session_background: Sessions.Background,
   store: Sessions.Store,
   do_store: Boolean,
   log: Logger,
@@ -247,14 +245,13 @@
   val numa_node: Option[Int],
   command_timings0: List[Properties.T]
 ) {
+  def session_name: String = session_background.session_name
+  val info: Sessions.Info = session_background.sessions_structure(session_name)
   val options: Options = NUMA.policy_options(info.options, numa_node)
 
-  private val session_background = deps.background(session_name)
-
   private val future_result: Future[Process_Result] =
     Future.thread("build", uninterruptible = true) {
       val parent = info.parent.getOrElse("")
-      val result_base = deps(session_name)
 
       val env =
         Isabelle_System.settings(
@@ -279,9 +276,9 @@
           override val cache: Term.Cache = store.cache
 
           override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = {
-            result_base.load_commands.get(name.expand) match {
+            session_background.base.load_commands.get(name.expand) match {
               case Some(spans) =>
-                val syntax = result_base.theory_syntax(name)
+                val syntax = session_background.base.theory_syntax(name)
                 Command.build_blobs_info(syntax, name, spans)
               case None => Command.Blobs_Info.none
             }
@@ -487,7 +484,7 @@
           if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
             using(Export.open_database_context(store)) { database_context =>
               val documents =
-                using(database_context.open_session(deps.background(session_name))) {
+                using(database_context.open_session(session_background)) {
                   session_context =>
                     Document_Build.build_documents(
                       Document_Build.context(session_context, progress = progress),
@@ -514,7 +511,7 @@
               case _ => None
             }).toMap
         val used_theory_timings =
-          for { (name, _) <- deps(session_name).used_theories }
+          for { (name, _) <- session_background.base.used_theories }
             yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
 
         val more_output =