--- a/src/Pure/Thy/document_build.scala Sun Dec 18 13:53:05 2022 +0100
+++ b/src/Pure/Thy/document_build.scala Sun Dec 18 14:39:35 2022 +0100
@@ -109,7 +109,21 @@
}
- /* context */
+ /* background context */
+
+ def session_background(
+ options: Options,
+ session: String,
+ dirs: List[Path] = Nil,
+ progress: Progress = new Progress
+ ): Sessions.Background = {
+ Sessions.load_structure(options + "document=pdf", dirs = dirs).
+ selection_deps(Sessions.Selection.session(session), progress = progress).
+ background(session)
+ }
+
+
+ /* document context */
val texinputs: Path = Path.explode("~~/lib/texinputs")
@@ -507,17 +521,12 @@
dirs = dirs, progress = progress, verbose = verbose_build)
if (!build_results.ok) error("Failed to build session " + quote(session))
- val deps =
- Sessions.load_structure(options + "document=pdf", dirs = dirs).
- selection_deps(Sessions.Selection.session(session))
-
- val session_background = deps.background(session)
-
if (output_sources.isEmpty && output_pdf.isEmpty) {
progress.echo_warning("No output directory")
}
- using(Export.open_session_context(build_results.store, session_background)) {
+ val background = session_background(options, session, dirs = dirs)
+ using(Export.open_session_context(build_results.store, background)) {
session_context =>
build_documents(
context(session_context, progress = progress),
--- a/src/Pure/Thy/sessions.scala Sun Dec 18 13:53:05 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Sun Dec 18 14:39:35 2022 +0100
@@ -102,6 +102,9 @@
nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
}
+
+ /* background context */
+
sealed case class Background(
base: Base,
sessions_structure: Structure = Structure.empty,