--- 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>\<open>-R\<close> specifies an explicit repository root directory. The default
is to derive it from the current directory, searching upwards until a
suitable \<^verbatim>\<open>.hg\<close> directory is found.
+
+ \<^medskip> Option \<^verbatim>\<open>-T\<close> indicates a thorough check of file content; the default is to
+ consider files with equal time and size already as equal.
\<close>
subsubsection \<open>Examples\<close>
--- 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)
}
)
}
--- 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 /" + _))
}
)
}
--- 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 +