src/Pure/Thy/document_build.scala
changeset 76717 4db685231326
parent 76677 899e83d90756
child 76731 872fc664cd99
--- a/src/Pure/Thy/document_build.scala	Tue Dec 20 16:34:13 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Tue Dec 20 18:33:51 2022 +0100
@@ -115,10 +115,11 @@
     options: Options,
     session: String,
     dirs: List[Path] = Nil,
-    progress: Progress = new Progress
+    progress: Progress = new Progress,
+    verbose: Boolean = false
   ): Sessions.Background = {
       Sessions.load_structure(options + "document=pdf", dirs = dirs).
-        selection_deps(Sessions.Selection.session(session), progress = progress).
+        selection_deps(Sessions.Selection.session(session), progress = progress, verbose = verbose).
         background(session)
   }