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