# HG changeset patch
# User wenzelm
# Date 1655113726 -7200
# Node ID 5340239ff468c5679b779327444214c83c27a0cd
# Parent  cf69c9112d098e891e40004c239ed768ba1e9196
clarified options of "isabelle hg_sync" vs. "isabelle sync";

diff -r cf69c9112d09 -r 5340239ff468 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Mon Jun 13 11:35:00 2022 +0200
+++ b/src/Doc/System/Misc.thy	Mon Jun 13 11:48:46 2022 +0200
@@ -314,6 +314,8 @@
                  (e.g. "protect /foo" to avoid deletion)
     -R ROOT      explicit repository root directory
                  (default: implicit from current directory)
+    -S           robust (but less portable) treatment of spaces in
+                 file and directory names on the target
     -T           thorough treatment of file content and directory times
     -n           no changes: dry-run
     -r REV       explicit revision (default: state of working directory)
@@ -353,6 +355,12 @@
 
   \<^medskip> Option \<^verbatim>\<open>-p\<close> specifies an explicit port for the SSH connection underlying
   \<^verbatim>\<open>rsync\<close>.
+
+  \<^medskip> Option \<^verbatim>\<open>-S\<close> uses \<^verbatim>\<open>rsync --protect-args\<close> to work robustly with spaces or
+  special characters of the shell. This requires at least \<^verbatim>\<open>rsync 3.0.0\<close>,
+  which is not always available --- notably on macOS. Assuming traditional
+  Unix-style naming of files and directories, it is safe to omit this option
+  for the sake of portability.
 \<close>
 
 subsubsection \<open>Examples\<close>
diff -r cf69c9112d09 -r 5340239ff468 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Jun 13 11:35:00 2022 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Jun 13 11:48:46 2022 +0200
@@ -896,7 +896,7 @@
   sub-directory with the literal name \<^verbatim>\<open>AFP\<close>; thus it can be easily included
   elsewhere, e.g. @{tool build}~\<^verbatim>\<open>-d\<close>~\<^verbatim>\<open>'~~/AFP'\<close> on the remote side.
 
-  \<^medskip> Options \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-v\<close> are the same as the underlying
+  \<^medskip> Options \<^verbatim>\<open>-S\<close>, \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-v\<close> are the same as the underlying
   @{tool hg_sync}.
 
   \<^medskip> Options \<^verbatim>\<open>-r\<close> and \<^verbatim>\<open>-a\<close> are the same as option \<^verbatim>\<open>-r\<close> for @{tool hg_sync},
@@ -933,11 +933,6 @@
   remains unchanged. Over time, this may lead to unused garbage, due to
   changes in session names or the Poly/ML version. Option \<^verbatim>\<open>-H\<close> helps to avoid
   wasting file-system space.
-
-  \<^medskip> Option \<^verbatim>\<open>-S\<close> uses \<^verbatim>\<open>rsync --protect-args\<close>, but this requires at least
-  \<^verbatim>\<open>rsync 3.0.0\<close>, while macOS might only provide \<^verbatim>\<open>rsync 2.9.x\<close>. Since
-  Isabelle + AFP don't use spaces or other special characters, it is usually
-  safe to omit this non-portable option.
 \<close>
 
 subsubsection \<open>Examples\<close>
diff -r cf69c9112d09 -r 5340239ff468 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Mon Jun 13 11:35:00 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Mon Jun 13 11:48:46 2022 +0200
@@ -562,6 +562,7 @@
       Scala_Project.here, { args =>
         var filter: List[String] = Nil
         var root: Option[Path] = None
+        var protect_args = false
         var thorough = false
         var dry_run = false
         var rev = ""
@@ -576,6 +577,8 @@
                  (e.g. "protect /foo" to avoid deletion)
     -R ROOT      explicit repository root directory
                  (default: implicit from current directory)
+    -S           robust (but less portable) treatment of spaces in
+                 file and directory names on the target
     -T           thorough treatment of file content and directory times
     -n           no changes: dry-run
     -r REV       explicit revision (default: state of working directory)
@@ -587,6 +590,7 @@
 """,
           "F:" -> (arg => filter = filter ::: List(arg)),
           "R:" -> (arg => root = Some(Path.explode(arg))),
+          "S" -> (_ => protect_args = true),
           "T" -> (_ => thorough = true),
           "n" -> (_ => dry_run = true),
           "r:" -> (arg => rev = arg),
@@ -606,7 +610,7 @@
             case Some(dir) => repository(dir)
             case None => the_repository(Path.current)
           }
-        val context = Rsync.Context(progress, port = port)
+        val context = Rsync.Context(progress, port = port, protect_args = protect_args)
         hg.sync(context, target, verbose = verbose, thorough = thorough,
           dry_run = dry_run, filter = filter, rev = rev)
       }