tuned signature;
authorwenzelm
Wed, 21 Dec 2022 14:14:02 +0100
changeset 76731 872fc664cd99
parent 76730 1b8dd8c0492f
child 76732 0ba6f360d38a
tuned signature;
src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed Dec 21 14:00:00 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Dec 21 14:14:02 2022 +0100
@@ -141,7 +141,7 @@
   final class Context private[Document_Build](
     val session_context: Export.Session_Context,
     document_session: Option[Sessions.Base],
-    val progress: Progress = new Progress
+    val progress: Progress
   ) {
     context =>
 
@@ -526,8 +526,8 @@
             progress.echo_warning("No output directory")
           }
 
-          val background = session_background(options, session, dirs = dirs)
-          using(Export.open_session_context(build_results.store, background)) {
+          val session_background = Document_Build.session_background(options, session, dirs = dirs)
+          using(Export.open_session_context(build_results.store, session_background)) {
             session_context =>
               build_documents(
                 context(session_context, progress = progress),