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
     }
 }