removed unused arguments: avoid ambiguity concerning progress/verbose;
authorwenzelm
Sun, 05 Mar 2023 16:26:59 +0100
changeset 77520 84aa349ed597
parent 77519 12ace037d05e
child 77521 5642de4d225d
removed unused arguments: avoid ambiguity concerning progress/verbose;
src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sun Mar 05 16:14:48 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sun Mar 05 16:26:59 2023 +0100
@@ -116,13 +116,10 @@
   def session_background(
     options: Options,
     session: String,
-    dirs: List[Path] = Nil,
-    progress: Progress = new Progress,
-    verbose: Boolean = false
+    dirs: List[Path] = Nil
   ): Sessions.Background = {
       Sessions.load_structure(options + "document", dirs = dirs).
-        selection_deps(Sessions.Selection.session(session), progress = progress, verbose = verbose).
-        background(session)
+        selection_deps(Sessions.Selection.session(session)).background(session)
   }