--- a/src/Pure/Tools/build_job.scala Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/Tools/build_job.scala Fri Dec 16 17:51:52 2022 +0100
@@ -249,7 +249,7 @@
) {
val options: Options = NUMA.policy_options(info.options, numa_node)
- private val base_info = deps.base_info(session_name)
+ private val session_background = deps.background(session_name)
private val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
@@ -274,7 +274,7 @@
else Nil
val resources =
- new Resources(base_info.sessions_structure, base_info.base, log = log,
+ new Resources(session_background.sessions_structure, session_background.base, log = log,
command_timings = command_timings0)
val session =
new Session(options, resources) {
@@ -451,7 +451,7 @@
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
val process =
- Isabelle_Process.start(session, options, base_info, store,
+ Isabelle_Process.start(session, options, session_background, store,
logic = parent, raw_ml_system = is_pure,
use_prelude = use_prelude, eval_main = eval_main,
cwd = info.dir.file, env = env)
@@ -489,7 +489,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.base_info(session_name))) {
+ using(database_context.open_session(deps.background(session_name))) {
session_context =>
Document_Build.build_documents(
Document_Build.context(session_context, progress = progress),