# HG changeset patch
# User wenzelm
# Date 1678026302 -3600
# Node ID ede77a627b3a4ef648c6af32e2e96571f78d49c8
# Parent  71e3e144dc08b83c000c397fddcabefe318eedf1
tuned;

diff -r 71e3e144dc08 -r ede77a627b3a src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Sun Mar 05 15:19:53 2023 +0100
+++ b/src/Pure/General/rsync.scala	Sun Mar 05 15:25:02 2023 +0100
@@ -33,6 +33,7 @@
     filter: List[String] = Nil,
     args: List[String] = Nil
   ): Process_Result = {
+    val progress = context.progress
     val script =
       context.command +
         (if (verbose) " --verbose" else "") +
@@ -43,7 +44,7 @@
         (if (list) " --list-only --no-human-readable" else "") +
         filter.map(s => " --filter=" + Bash.string(s)).mkString +
         if_proper(args, " " + Bash.strings(args))
-    context.progress.bash(script, echo = true)
+    progress.bash(script, echo = true)
   }
 
   def init(context: Context, target: String,
diff -r 71e3e144dc08 -r ede77a627b3a src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sun Mar 05 15:19:53 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sun Mar 05 15:25:02 2023 +0100
@@ -442,8 +442,9 @@
       directory: Directory,
       verbose: Boolean
     ): Document_Output = {
+      val progress = context.progress
       val result =
-        context.progress.bash(
+        progress.bash(
           build_script(context, directory),
           cwd = directory.doc_dir.file,
           echo = verbose,
diff -r 71e3e144dc08 -r ede77a627b3a src/Pure/Tools/sync.scala
--- a/src/Pure/Tools/sync.scala	Sun Mar 05 15:19:53 2023 +0100
+++ b/src/Pure/Tools/sync.scala	Sun Mar 05 15:25:02 2023 +0100
@@ -44,6 +44,8 @@
     afp_root: Option[Path] = None,
     afp_rev: String = ""
   ): Unit = {
+    val progress = context.progress
+
     val hg = Mercurial.self_repository()
     val afp_hg = afp_root.map(Mercurial.repository(_))
 
@@ -56,14 +58,14 @@
         contents = contents, filter = filter ::: more_filter)
     }
 
-    context.progress.echo_if(verbose, "\n* Isabelle repository:")
+    progress.echo_if(verbose, "\n* Isabelle repository:")
     val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**")
     sync(hg, target, rev,
       contents = List(File.content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
       filter = filter_heaps ::: List("protect /AFP"))
 
     for (hg <- afp_hg) {
-      context.progress.echo_if(verbose, "\n* AFP repository:")
+      progress.echo_if(verbose, "\n* AFP repository:")
       sync(hg, Url.append_path(target, "AFP"), afp_rev)
     }
 
@@ -71,7 +73,7 @@
       find_images(options, session_images,
         dirs = afp_root.map(_ + Path.explode("thys")).toList)
     if (images.nonEmpty) {
-      context.progress.echo_if(verbose, "\n* Session images:")
+      progress.echo_if(verbose, "\n* Session images:")
       val heaps = Url.append_path(target, "heaps/")
       Rsync.exec(context, verbose = verbose, thorough = thorough, dry_run = dry_run,
         args = List("--relative", "--") ::: images ::: List(heaps)).check