support filter rules, notably "protect";

--- a/src/Pure/General/mercurial.scala	Sun May 29 13:13:45 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Sun May 29 15:16:49 2022 +0200
@@ -255,13 +255,14 @@
       progress: Progress = new Progress,
       verbose: Boolean = false,
       dry_run: Boolean = false,
-      clean: Boolean = false
+      clean: Boolean = false,
+      filter: List[String] = Nil
     ): Unit = {
       Isabelle_System.with_tmp_file("exclude") { exclude_path =>
         val exclude = status(options = "--unknown --ignored --no-status")
         File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
         Isabelle_System.rsync(
-          progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
+          progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, filter = filter,
           args = List("--prune-empty-dirs", "--exclude-from=" + exclude_path.implode,
             "--", ssh.rsync_url + root.expand.implode + "/.", target)
         ).check
@@ -469,6 +470,7 @@
     Isabelle_Tool("hg_sync", "synchronize Mercurial repository working directory",
       Scala_Project.here, { args =>
         var clean = false
+        var protect: List[String] = Nil
         var root: Option[Path] = None
         var dry_run = false
         var verbose = false
@@ -479,6 +481,7 @@
   Options are:
     -C           clean all unknown/ignored files on target
                  (potentially DANGEROUS: use with option -f to confirm)
+    -P NAME      protect NAME within TARGET from deletion
     -R ROOT      explicit repository root directory
                  (default: implicit from current directory)
     -f           force changes: no dry-run
@@ -489,6 +492,7 @@
   which can be local or remote (using notation of rsync).
 """,
           "C" -> { _ => clean = true; dry_run = true },
+          "P:" -> (arg => protect = protect ::: List(arg)),
           "R:" -> (arg => root = Some(Path.explode(arg))),
           "f" -> (_ => dry_run = false),
           "n" -> (_ => dry_run = true),
@@ -507,7 +511,9 @@
             case Some(dir) => repository(dir)
             case None => the_repository(Path.current)
           }
-        hg.sync(target, verbose = verbose, dry_run = dry_run, clean = clean, progress = progress)
+        hg.sync(target, verbose = verbose, dry_run = dry_run, clean = clean,
+          filter = protect.map("protect /" + _),
+          progress = progress)
       }
     )
 }

--- a/src/Pure/System/isabelle_system.scala	Sun May 29 13:13:45 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun May 29 15:16:49 2022 +0200
@@ -426,6 +426,7 @@
     verbose: Boolean = false,
     dry_run: Boolean = false,
     clean: Boolean = false,
+    filter: List[String] = Nil,
     args: List[String] = Nil
   ): Process_Result = {
     val script =
@@ -433,6 +434,7 @@
         (if (verbose || dry_run) " --verbose" else "") +
         (if (dry_run) " --dry-run" else "") +
         (if (clean) " --delete-excluded" else "") +
+        filter.map(s => " --filter=" + Bash.string(s)).mkString +
         (if (args.nonEmpty) " " + Bash.strings(args) else "")
     progress.bash(script, cwd = cwd, echo = true)
   }