# HG changeset patch
# User wenzelm
# Date 1654614430 -7200
# Node ID 68162e4f60a790db38e58544644da616cdb2da46
# Parent  ff8012edac89d445800d2d6c60170c3ae4747fe9
clarified signature: more explicit type Rsync.Context;

diff -r ff8012edac89 -r 68162e4f60a7 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Jun 07 16:47:57 2022 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Jun 07 17:07:10 2022 +0200
@@ -534,7 +534,8 @@
     def sync_repos(target: Path, accurate: Boolean = false,
       rev: String = "", afp_rev: String = "", afp: Boolean = false
     ): Unit = {
-      Sync_Repos.sync_repos(ssh.rsync_path(target), port = ssh.port, progress = progress,
+      val context = Rsync.Context(progress, port = ssh.port)
+      Sync_Repos.sync_repos(context, ssh.rsync_path(target),
         thorough = accurate, preserve_jars = !accurate,
         rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
     }
diff -r ff8012edac89 -r 68162e4f60a7 src/Pure/Admin/sync_repos.scala
--- a/src/Pure/Admin/sync_repos.scala	Tue Jun 07 16:47:57 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala	Tue Jun 07 17:07:10 2022 +0200
@@ -8,9 +8,7 @@
 
 
 object Sync_Repos {
-  def sync_repos(target: String,
-    progress: Progress = new Progress,
-    port: Int = SSH.default_port,
+  def sync_repos(context: Rsync.Context, target: String,
     verbose: Boolean = false,
     thorough: Boolean = false,
     preserve_jars: Boolean = false,
@@ -27,17 +25,17 @@
     def sync(hg: Mercurial.Repository, dest: String, r: String,
       contents: List[File.Content] = Nil, filter: List[String] = Nil
     ): Unit = {
-      hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose,
-        thorough = thorough, dry_run = dry_run, contents = contents, filter = filter ::: more_filter)
+      hg.sync(context, dest, rev = r, verbose = verbose, thorough = thorough, dry_run = dry_run,
+        contents = contents, filter = filter ::: more_filter)
     }
 
-    progress.echo_if(verbose, "\n* Isabelle repository:")
+    context.progress.echo_if(verbose, "\n* Isabelle repository:")
     sync(hg, target, rev,
       contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
       filter = List("protect /AFP"))
 
     for (hg <- afp_hg) {
-      progress.echo_if(verbose, "\n* AFP repository:")
+      context.progress.echo_if(verbose, "\n* AFP repository:")
       sync(hg, Rsync.append(target, "AFP"), afp_rev)
     }
   }
@@ -94,7 +92,8 @@
           }
 
         val progress = new Console_Progress
-        sync_repos(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
+        val context = Rsync.Context(progress, port = port)
+        sync_repos(context, target, verbose = verbose, thorough = thorough,
           preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root,
           afp_rev = afp_rev)
       }
diff -r ff8012edac89 -r 68162e4f60a7 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue Jun 07 16:47:57 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Tue Jun 07 17:07:10 2022 +0200
@@ -293,9 +293,7 @@
 
     def known_files(): List[String] = status(options = "--modified --added --clean --no-status")
 
-    def sync(target: String,
-      progress: Progress = new Progress,
-      port: Int = SSH.default_port,
+    def sync(context: Rsync.Context, target: String,
       verbose: Boolean = false,
       thorough: Boolean = false,
       dry_run: Boolean = false,
@@ -306,10 +304,10 @@
       require(ssh == SSH.Local, "local repository required")
 
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
-        Rsync.rsync_init(target, port = port)
+        Rsync.rsync_init(context, target)
 
         val list =
-          Rsync.rsync(port = port, list = true,
+          Rsync.rsync(context, list = true,
             args = List("--", Rsync.terminate(target))
           ).check.out_lines.filterNot(_.endsWith(" ."))
         if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
@@ -322,7 +320,7 @@
         val diff_content = if (is_changed) diff(rev = rev, options = "--git") else ""
         val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else ""
 
-        Rsync.rsync_init(target, port = port,
+        Rsync.rsync_init(context, target,
           contents =
             File.Content(Hg_Sync.PATH_ID, id_content) ::
             File.Content(Hg_Sync.PATH_LOG, log_content) ::
@@ -348,8 +346,9 @@
         val protect =
           (Hg_Sync.PATH :: contents.map(_.path))
             .map(path => "protect /" + File.standard_path(path))
-        Rsync.rsync(
-          progress = progress, port = port, verbose = verbose, thorough = thorough,
+        Rsync.rsync(context,
+          verbose = verbose,
+          thorough = thorough,
           dry_run = dry_run,
           clean = true,
           prune_empty_dirs = true,
@@ -606,7 +605,8 @@
             case Some(dir) => repository(dir)
             case None => the_repository(Path.current)
           }
-        hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
+        val context = Rsync.Context(progress, port = port)
+        hg.sync(context, target, verbose = verbose, thorough = thorough,
           dry_run = dry_run, filter = filter, rev = rev)
       }
     )
diff -r ff8012edac89 -r 68162e4f60a7 src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Tue Jun 07 16:47:57 2022 +0200
+++ b/src/Pure/General/rsync.scala	Tue Jun 07 17:07:10 2022 +0200
@@ -8,9 +8,13 @@
 
 
 object Rsync {
+  sealed case class Context(progress: Progress, port: Int = SSH.default_port) {
+    def command: String =
+      "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port)
+  }
+
   def rsync(
-    progress: Progress = new Progress,
-    port: Int = SSH.default_port,
+    context: Context,
     verbose: Boolean = false,
     thorough: Boolean = false,
     prune_empty_dirs: Boolean = false,
@@ -21,7 +25,7 @@
     args: List[String] = Nil
   ): Process_Result = {
     val script =
-      "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) +
+      context.command +
         (if (verbose) " --verbose" else "") +
         (if (thorough) " --ignore-times" else " --omit-dir-times") +
         (if (prune_empty_dirs) " --prune-empty-dirs" else "") +
@@ -30,17 +34,16 @@
         (if (list) " --list-only --no-human-readable" else "") +
         filter.map(s => " --filter=" + Bash.string(s)).mkString +
         (if (args.nonEmpty) " " + Bash.strings(args) else "")
-    progress.bash(script, echo = true)
+    context.progress.bash(script, echo = true)
   }
 
-  def rsync_init(target: String,
-    port: Int = SSH.default_port,
+  def rsync_init(context: Context, target: String,
     contents: List[File.Content] = Nil
   ): Unit =
     Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
       val init_dir = Isabelle_System.make_directory(tmp_dir + Path.explode("init"))
       contents.foreach(_.write(init_dir))
-      rsync(port = port, thorough = true,
+      rsync(context, thorough = true,
         args = List(File.bash_path(init_dir) + "/.", target)).check
     }