--- 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)
}
--- 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 =