clarified signature;
authorwenzelm
Sun, 18 Dec 2022 14:39:35 +0100
changeset 76677 899e83d90756
parent 76676 f572f5525e4b
child 76678 f34b923ff2c9
clarified signature;
src/Pure/Thy/document_build.scala
src/Pure/Thy/sessions.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),
--- 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,