# HG changeset patch
# User wenzelm
# Date 1653900720 -7200
# Node ID f08fd5048df31bb6c9e32c3586f44744c410dc64
# Parent  98d24c6516f6bec3a689dabc99ab9ee7d3bb678c
clarified command-line options;

diff -r 98d24c6516f6 -r f08fd5048df3 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Mon May 30 10:51:04 2022 +0200
+++ b/src/Doc/System/Misc.thy	Mon May 30 10:52:00 2022 +0200
@@ -313,7 +313,7 @@
   Options are:
     -C           clean all unknown/ignored files on target
                  (implies -n for testing; use option -f to confirm)
-    -P NAME      protect NAME within TARGET from deletion
+    -F RULE      add rsync filter RULE (e.g. "protect /foo" to avoid deletion)
     -R ROOT      explicit repository root directory
                  (default: implicit from current directory)
     -T           thorough check of file content (default: time and size)
@@ -342,8 +342,8 @@
   for ``dry-run'' with verbose output. A subsequent option \<^verbatim>\<open>-f\<close> is required
   to force actual deletions on the target.
 
-  \<^medskip> Option \<^verbatim>\<open>-P\<close> protects a given file or directory from deletion; multiple
-  \<^verbatim>\<open>-P\<close> options may be given to accumulate protected entries.
+  \<^medskip> Option \<^verbatim>\<open>-F\<close> adds a filter rule to the underlying \<^verbatim>\<open>rsync\<close> command;
+  multiple \<^verbatim>\<open>-F\<close> options may be given to accumulate a list of rules.
 
   \<^medskip> Option \<^verbatim>\<open>-R\<close> specifies an explicit repository root directory. The default
   is to derive it from the current directory, searching upwards until a
@@ -356,9 +356,8 @@
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  Synchronize the Isabelle repository onto a remote host, while
-  protecting a copy of AFP inside of it (without changing that):
-  @{verbatim [display] \<open>  isabelle hg_sync -R '$ISABELLE_HOME' -P AFP -C testmachine:test/isabelle\<close>}
+  Synchronize the Isabelle repository onto a remote host:
+  @{verbatim [display] \<open>  isabelle hg_sync -R '$ISABELLE_HOME' -C testmachine:test/isabelle\<close>}
 
   So far, this is only a dry run. In a realistic situation, it requires
   consecutive options \<^verbatim>\<open>-C -f\<close> as confirmation.
diff -r 98d24c6516f6 -r f08fd5048df3 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Mon May 30 10:51:04 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Mon May 30 10:52:00 2022 +0200
@@ -486,7 +486,7 @@
     Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
       Scala_Project.here, { args =>
         var clean = false
-        var protect: List[String] = Nil
+        var filter: List[String] = Nil
         var root: Option[Path] = None
         var thorough = false
         var dry_run = false
@@ -499,7 +499,7 @@
   Options are:
     -C           clean all unknown/ignored files on target
                  (implies -n for testing; use option -f to confirm)
-    -P NAME      protect NAME within TARGET from deletion
+    -F RULE      add rsync filter RULE (e.g. "protect /foo" to avoid deletion)
     -R ROOT      explicit repository root directory
                  (default: implicit from current directory)
     -T           thorough check of file content (default: time and size)
@@ -512,7 +512,7 @@
   which can be local or remote (using notation of rsync).
 """,
           "C" -> { _ => clean = true; dry_run = true },
-          "P:" -> (arg => protect = protect ::: List(arg)),
+          "F:" -> (arg => filter = filter ::: List(arg)),
           "R:" -> (arg => root = Some(Path.explode(arg))),
           "T" -> (_ => thorough = true),
           "f" -> (_ => dry_run = false),
@@ -534,8 +534,7 @@
             case None => the_repository(Path.current)
           }
         hg.sync(target, progress = progress, verbose = verbose, thorough = thorough,
-          dry_run = dry_run, clean = clean, rev = rev,
-          filter = protect.map("protect /" + _))
+          dry_run = dry_run, clean = clean, filter = filter, rev = rev)
       }
     )
 }