# HG changeset patch
# User wenzelm
# Date 1680973198 -7200
# Node ID ed68c546746cd19ff44d51657ced8215f1531f79
# Parent  59ab77f7d021eac34a3ec0e747527b1f24ade3a4
misc tuning and clarification;

diff -r 59ab77f7d021 -r ed68c546746c src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Sat Apr 08 18:46:17 2023 +0200
+++ b/src/Pure/General/rsync.scala	Sat Apr 08 18:59:58 2023 +0200
@@ -16,27 +16,27 @@
       protect_args: Boolean = true  // requires rsync 3.0.0, or later
     ): Context = {
       val directory = Components.provide(Component_Rsync.home, ssh = ssh, progress = progress)
-      val remote_program = Component_Rsync.remote_program(directory)
-      val rsync_path = quote(File.standard_path(remote_program))
-      new Context(progress, ssh, rsync_path, archive, protect_args)
+      new Context(directory, progress, archive, protect_args)
     }
   }
 
   final class Context private(
+    directory: Components.Directory,
     val progress: Progress,
-    val ssh: SSH.System,
-    rsync_path: String,
     archive: Boolean,
     protect_args: Boolean,
   ) {
-    def no_progress: Context = new Context(new Progress, ssh, rsync_path, archive, protect_args)
-    def no_archive: Context = new Context(progress, ssh, rsync_path, false, protect_args)
+    def no_progress: Context = new Context(directory, new Progress, archive, protect_args)
+    def no_archive: Context = new Context(directory, progress, false, protect_args)
+
+    def ssh: SSH.System = directory.ssh
 
     def command: String = {
+      val program = Component_Rsync.remote_program(directory)
       val ssh_command = ssh.client_command
       File.bash_path(Component_Rsync.local_program) +
         if_proper(ssh_command, " --rsh=" + Bash.string(ssh_command)) +
-        " --rsync-path=" + Bash.string(rsync_path) +
+        " --rsync-path=" + Bash.string(quote(File.standard_path(program))) +
         (if (archive) " --archive" else "") +
         (if (protect_args) " --protect-args" else "")
     }