merged

--- a/src/Pure/Admin/sync_repos.scala	Tue Jun 07 17:53:33 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala	Tue Jun 07 19:23:47 2022 +0200
@@ -45,6 +45,7 @@
       Scala_Project.here, { args =>
         var afp_root: Option[Path] = None
         var preserve_jars = false
+        var protect_args = false
         var thorough = false
         var afp_rev = ""
         var dry_run = false
@@ -58,6 +59,7 @@
   Options are:
     -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
     -J           preserve *.jar files
+    -S           robust (but less portable) treatment of spaces in directory names
     -T           thorough treatment of file content and directory times
     -a REV       explicit AFP revision (default: state of working directory)
     -n           no changes: dry-run
@@ -77,6 +79,7 @@
 """,
           "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
           "J" -> (_ => preserve_jars = true),
+          "S" -> (_ => protect_args = true),
           "T" -> (_ => thorough = true),
           "a:" -> (arg => afp_rev = arg),
           "n" -> (_ => dry_run = true),
@@ -92,7 +95,7 @@
           }
 
         val progress = new Console_Progress
-        val context = Rsync.Context(progress, port = port)
+        val context = Rsync.Context(progress, port = port, protect_args = protect_args)
         sync_repos(context, target, verbose = verbose, thorough = thorough,
           preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root,
           afp_rev = afp_rev)

--- a/src/Pure/General/mercurial.scala	Tue Jun 07 17:53:33 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Tue Jun 07 19:23:47 2022 +0200
@@ -304,12 +304,13 @@
       require(ssh == SSH.Local, "local repository required")
 
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
-        Rsync.init(context, target)
+        val context0 = context.copy(progress = new Progress)
+
+        Rsync.init(context0, target)
 
         val list =
-          Rsync.exec(context, list = true,
-            args = List("--", Rsync.terminate(target))
-          ).check.out_lines.filterNot(_.endsWith(" ."))
+          Rsync.exec(context0, list = true, args = List("--", Rsync.terminate(target)))
+            .check.out_lines.filterNot(_.endsWith(" ."))
         if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
           error("No .hg_sync meta data in " + quote(target))
         }
@@ -320,7 +321,7 @@
         val diff_content = if (is_changed) diff(rev = rev, options = "--git") else ""
         val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else ""
 
-        Rsync.init(context, target,
+        Rsync.init(context0, target,
           contents =
             File.Content(Hg_Sync.PATH_ID, id_content) ::
             File.Content(Hg_Sync.PATH_LOG, log_content) ::

--- a/src/Pure/General/rsync.scala	Tue Jun 07 17:53:33 2022 +0200
+++ b/src/Pure/General/rsync.scala	Tue Jun 07 19:23:47 2022 +0200
@@ -49,8 +49,11 @@
     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, thorough = true,
-        args = List(File.bash_path(init_dir) + "/.", target)).check
+      exec(context.copy(archive = false),
+        thorough = true,
+        args =
+          List(if (contents.nonEmpty) "--archive" else "--dirs",
+            File.bash_path(init_dir) + "/.", target)).check
     }
 
   def terminate(target: String): String =