# HG changeset patch # User wenzelm # Date 1653830209 -7200 # Node ID f1d204a4d7950b36ff53551e9d6dd716ffb41e0c # Parent d16dd2d1b50aaaf546269c950ed5f960d1bbb488 support filter rules, notably "protect"; diff -r d16dd2d1b50a -r f1d204a4d795 src/Pure/General/mercurial.scala --- 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) } ) } diff -r d16dd2d1b50a -r f1d204a4d795 src/Pure/System/isabelle_system.scala --- 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) }