# HG changeset patch # User wenzelm # Date 1653899516 -7200 # Node ID 167660a8f99e41b7eff31da7640a397c1cf39867 # Parent ba4ed9a50be3bd2dce8837c5378f74de3019b197 support thorough check of file content; diff -r ba4ed9a50be3 -r 167660a8f99e src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Mon May 30 10:15:27 2022 +0200 +++ b/src/Doc/System/Misc.thy Mon May 30 10:31:56 2022 +0200 @@ -316,6 +316,7 @@ -P NAME protect NAME within TARGET from deletion -R ROOT explicit repository root directory (default: implicit from current directory) + -T thorough check of file content (default: time and size) -f force changes: no dry-run -n no changes: dry-run -r REV explicit revision (default: state of working directory) @@ -347,6 +348,9 @@ \<^medskip> Option \<^verbatim>\-R\ specifies an explicit repository root directory. The default is to derive it from the current directory, searching upwards until a suitable \<^verbatim>\.hg\ directory is found. + + \<^medskip> Option \<^verbatim>\-T\ indicates a thorough check of file content; the default is to + consider files with equal time and size already as equal. \ subsubsection \Examples\ diff -r ba4ed9a50be3 -r 167660a8f99e src/Pure/Admin/sync_repos.scala --- a/src/Pure/Admin/sync_repos.scala Mon May 30 10:15:27 2022 +0200 +++ b/src/Pure/Admin/sync_repos.scala Mon May 30 10:31:56 2022 +0200 @@ -11,6 +11,7 @@ def sync_repos(target: String, progress: Progress = new Progress, verbose: Boolean = false, + thorough: Boolean = false, dry_run: Boolean = false, clean: Boolean = false, rev: String = "", @@ -23,8 +24,8 @@ val afp_hg = afp_root.map(Mercurial.repository(_)) def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit = - hg.sync(dest, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, - rev = r, filter = filter) + hg.sync(dest, rev = r, progress = progress, verbose = verbose, thorough = thorough, + dry_run = dry_run, clean = clean, filter = filter) progress.echo("\n* Isabelle repository:") sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect etc/ISABELLE_ID")) @@ -33,7 +34,8 @@ Isabelle_System.with_tmp_dir("sync_repos") { tmp_dir => val id_path = tmp_dir + Path.explode("ISABELLE_ID") File.write(id_path, isabelle_hg.id(rev = rev)) - Isabelle_System.rsync(args = List(File.standard_path(id_path), target_dir + "etc/")) + Isabelle_System.rsync(thorough = thorough, + args = List(File.standard_path(id_path), target_dir + "etc/")) } } @@ -48,6 +50,7 @@ Scala_Project.here, { args => var afp_root: Option[Path] = None var clean = false + var thorough = false var afp_rev = "" var dry_run = false var rev = "" @@ -60,6 +63,7 @@ -A ROOT include AFP with given root directory -C clean all unknown/ignored files on target (implies -n for testing; use option -f to confirm) + -T thorough check of file content (default: time and size) -a REV explicit AFP revision (default: state of working directory) -f force changes: no dry-run -n no changes: dry-run @@ -74,6 +78,7 @@ """, "A:" -> (arg => afp_root = Some(Path.explode(arg))), "C" -> { _ => clean = true; dry_run = true }, + "T" -> (_ => thorough = true), "a:" -> (arg => afp_rev = arg), "f" -> (_ => dry_run = false), "n" -> (_ => dry_run = true), @@ -88,8 +93,8 @@ } val progress = new Console_Progress - sync_repos(target, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, - rev = rev, afp_root = afp_root, afp_rev = afp_rev) + sync_repos(target, progress = progress, verbose = verbose, thorough = thorough, + dry_run = dry_run, clean = clean, rev = rev, afp_root = afp_root, afp_rev = afp_rev) } ) } diff -r ba4ed9a50be3 -r 167660a8f99e src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Mon May 30 10:15:27 2022 +0200 +++ b/src/Pure/General/mercurial.scala Mon May 30 10:31:56 2022 +0200 @@ -254,6 +254,7 @@ def sync(target: String, progress: Progress = new Progress, verbose: Boolean = false, + thorough: Boolean = false, dry_run: Boolean = false, clean: Boolean = false, filter: List[String] = Nil, @@ -278,7 +279,8 @@ (Nil, source) } Isabelle_System.rsync( - progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, filter = filter, + progress = progress, verbose = verbose, thorough = thorough, + dry_run = dry_run, clean = clean, filter = filter, args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target)) } } @@ -486,6 +488,7 @@ var clean = false var protect: List[String] = Nil var root: Option[Path] = None + var thorough = false var dry_run = false var rev = "" var verbose = false @@ -499,6 +502,7 @@ -P NAME protect NAME within TARGET from deletion -R ROOT explicit repository root directory (default: implicit from current directory) + -T thorough check of file content (default: time and size) -f force changes: no dry-run -n no changes: dry-run -r REV explicit revision (default: state of working directory) @@ -510,6 +514,7 @@ "C" -> { _ => clean = true; dry_run = true }, "P:" -> (arg => protect = protect ::: List(arg)), "R:" -> (arg => root = Some(Path.explode(arg))), + "T" -> (_ => thorough = true), "f" -> (_ => dry_run = false), "n" -> (_ => dry_run = true), "r:" -> (arg => rev = arg), @@ -528,8 +533,9 @@ case Some(dir) => repository(dir) case None => the_repository(Path.current) } - hg.sync(target, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, - filter = protect.map("protect /" + _), rev = rev) + hg.sync(target, progress = progress, verbose = verbose, thorough = thorough, + dry_run = dry_run, clean = clean, rev = rev, + filter = protect.map("protect /" + _)) } ) } diff -r ba4ed9a50be3 -r 167660a8f99e src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon May 30 10:15:27 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon May 30 10:31:56 2022 +0200 @@ -424,6 +424,7 @@ cwd: JFile = null, progress: Progress = new Progress, verbose: Boolean = false, + thorough: Boolean = false, dry_run: Boolean = false, clean: Boolean = false, filter: List[String] = Nil, @@ -432,6 +433,7 @@ val script = "rsync --protect-args --archive" + (if (verbose || dry_run) " --verbose" else "") + + (if (thorough) " --ignore-times" else "") + (if (dry_run) " --dry-run" else "") + (if (clean) " --delete-excluded" else "") + filter.map(s => " --filter=" + Bash.string(s)).mkString +