diff -r 127d077cccfe -r fb61887c069a src/Pure/General/rsync.scala --- a/src/Pure/General/rsync.scala Sat Apr 08 10:24:54 2023 +0200 +++ b/src/Pure/General/rsync.scala Sat Apr 08 16:37:54 2023 +0200 @@ -9,17 +9,22 @@ object Rsync { sealed case class Context(progress: Progress, - ssh_port: Int = 0, - ssh_control_path: String = "", + ssh: SSH.System = SSH.Local, archive: Boolean = true, protect_args: Boolean = true // requires rsync 3.0.0, or later ) { def command: String = { - val ssh_command = SSH.client_command(port = ssh_port, control_path = ssh_control_path) - "rsync --rsh=" + Bash.string(ssh_command) + + val ssh_command = ssh.client_command + "rsync" + + if_proper(ssh_command, " --rsh=" + Bash.string(ssh_command)) + (if (archive) " --archive" else "") + (if (protect_args) " --protect-args" else "") } + + def target(path: Path, direct: Boolean = false): String = { + val s = ssh.rsync_path(path) + if (direct) Url.direct_path(s) else s + } } def exec( @@ -46,7 +51,7 @@ progress.bash(script, echo = true) } - def init(context: Context, target: String, + def init(context: Context, target: Path, contents: List[File.Content] = Nil ): Unit = Isabelle_System.with_tmp_dir("sync") { tmp_dir => @@ -56,6 +61,6 @@ thorough = true, args = List(if (contents.nonEmpty) "--archive" else "--dirs", - File.bash_path(init_dir) + "/.", target)).check + File.bash_path(init_dir) + "/.", context.target(target))).check } }