# HG changeset patch
# User wenzelm
# Date 1680967215 -7200
# Node ID b20ac2c26ea37d3c9c1e0f809b87242e6744e585
# Parent  3badbb7bc7ed54c59e6428773043b2d67843189c
clarified signature: more abstract;

diff -r 3badbb7bc7ed -r b20ac2c26ea3 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Apr 08 16:59:20 2023 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Apr 08 17:20:15 2023 +0200
@@ -548,7 +548,7 @@
     def sync(target: Path, accurate: Boolean = false,
       rev: String = "", afp_rev: String = "", afp: Boolean = false
     ): Unit = {
-      val context = Rsync.Context(progress, ssh = ssh, protect_args = protect_args)
+      val context = Rsync.Context(progress = progress, ssh = ssh, protect_args = protect_args)
       Sync.sync(ssh.options, context, target,
         thorough = accurate, preserve_jars = !accurate,
         rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
diff -r 3badbb7bc7ed -r b20ac2c26ea3 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Apr 08 16:59:20 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Apr 08 17:20:15 2023 +0200
@@ -307,9 +307,7 @@
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
         Hg_Sync.check_directory(target, ssh = context.ssh)
 
-        val context0 = context.copy(progress = new Progress)
-
-        Rsync.init(context0, target)
+        Rsync.init(context.no_progress, target)
 
         val id_content = id(rev = rev)
         val is_changed = id_content.endsWith("+")
@@ -317,7 +315,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.init(context0, target,
+        Rsync.init(context.no_progress, target,
           contents =
             File.content(Hg_Sync.PATH_ID, id_content) ::
             File.content(Hg_Sync.PATH_LOG, log_content) ::
@@ -613,7 +611,7 @@
           }
 
         using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
-          val context = Rsync.Context(progress, ssh = ssh, protect_args = protect_args)
+          val context = Rsync.Context(progress = progress, ssh = ssh, protect_args = protect_args)
           hg.sync(context, target, thorough = thorough, dry_run = dry_run,
             filter = filter, rev = rev)
         }
diff -r 3badbb7bc7ed -r b20ac2c26ea3 src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Sat Apr 08 16:59:20 2023 +0200
+++ b/src/Pure/General/rsync.scala	Sat Apr 08 17:20:15 2023 +0200
@@ -8,11 +8,24 @@
 
 
 object Rsync {
-  sealed case class Context(progress: Progress,
-    ssh: SSH.System = SSH.Local,
-    archive: Boolean = true,
-    protect_args: Boolean = true  // requires rsync 3.0.0, or later
+  object Context {
+    def apply(
+      progress: Progress = new Progress,
+      ssh: SSH.System = SSH.Local,
+      archive: Boolean = true,
+      protect_args: Boolean = true  // requires rsync 3.0.0, or later
+    ): Context = new Context(progress, ssh, archive, protect_args)
+  }
+
+  final class Context private(
+    val progress: Progress,
+    val ssh: SSH.System,
+    archive: Boolean,
+    protect_args: Boolean
   ) {
+    def no_progress: Context = new Context(new Progress, ssh, archive, protect_args)
+    def no_archive: Context = new Context(progress, ssh, false, protect_args)
+
     def command: String = {
       val ssh_command = ssh.client_command
       "rsync" +
@@ -55,7 +68,7 @@
     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))
-      exec(context.copy(archive = false),
+      exec(context.no_archive,
         thorough = true,
         args =
           List(if (contents.nonEmpty) "--archive" else "--dirs",
diff -r 3badbb7bc7ed -r b20ac2c26ea3 src/Pure/Tools/sync.scala
--- a/src/Pure/Tools/sync.scala	Sat Apr 08 16:59:20 2023 +0200
+++ b/src/Pure/Tools/sync.scala	Sat Apr 08 17:20:15 2023 +0200
@@ -142,7 +142,7 @@
         val progress = new Console_Progress(verbose = verbose)
 
         using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
-          val context = Rsync.Context(progress, ssh = ssh, protect_args = protect_args)
+          val context = Rsync.Context(progress = progress, ssh = ssh, protect_args = protect_args)
           sync(options, context, target, thorough = thorough, purge_heaps = purge_heaps,
             session_images = session_images, preserve_jars = preserve_jars, dry_run = dry_run,
             rev = rev, afp_root = afp_root, afp_rev = afp_rev)