# HG changeset patch # User wenzelm # Date 1671370775 -3600 # Node ID 899e83d907565d6e5477014d77f962562d18a276 # Parent f572f5525e4bb49194a9a8bcc366c6e913dd187b clarified signature; diff -r f572f5525e4b -r 899e83d90756 src/Pure/Thy/document_build.scala --- 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), diff -r f572f5525e4b -r 899e83d90756 src/Pure/Thy/sessions.scala --- 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,