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",