--- a/src/Doc/System/Misc.thy Sun May 29 17:37:43 2022 +0200
+++ b/src/Doc/System/Misc.thy Sun May 29 20:57:10 2022 +0200
@@ -303,9 +303,9 @@
section \<open>Mercurial repository synchronization\<close>
text \<open>
- The @{tool_def hg_sync} tool synchronizes the working directory of a local
- Mercurial repository with a target directory, using
- \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close> notation for destinations.
+ The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with
+ a target directory, using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close>
+ notation for destinations.
@{verbatim [display]
\<open>Usage: isabelle hg_sync [OPTIONS] TARGET
@@ -318,15 +318,19 @@
(default: implicit from current directory)
-f force changes: no dry-run
-n no changes: dry-run
+ -r REV explicit revision (default: state of working directory)
-v verbose
- Synchronize Mercurial repository working directory with other TARGET,
+ Synchronize Mercurial repository with TARGET directory,
which can be local or remote (using notation of rsync).\<close>}
The \<^verbatim>\<open>TARGET\<close> specification can be a local or remote directory (via ssh),
using \<^verbatim>\<open>rsync\<close> notation (see examples below). The content is written
directly into the target, \<^emph>\<open>without\<close> creating a separate sub-directory.
+ \<^medskip> Option \<^verbatim>\<open>-r\<close> specifies an explicit revision of the repository; the default
+ is the current state of the working directory (which might be uncommitted).
+
\<^medskip> Option \<^verbatim>\<open>-v\<close> enables verbose mode. Option \<^verbatim>\<open>-n\<close> enables ``dry-run'' mode:
operations are only simulated and printed as in verbose mode. Option \<^verbatim>\<open>-f\<close>
disables ``dry-run'' mode and thus forces changes to be applied.
@@ -341,8 +345,8 @@
\<^verbatim>\<open>-P\<close> options may be given to accumulate protected entries.
\<^medskip> Option \<^verbatim>\<open>-R\<close> specifies an explicit repository root directory. The default
- is to derive it from the current working directory, searching upwards until
- a suitable \<^verbatim>\<open>.hg\<close> directory is found.
+ is to derive it from the current directory, searching upwards until a
+ suitable \<^verbatim>\<open>.hg\<close> directory is found.
\<close>
subsubsection \<open>Examples\<close>
--- a/src/Pure/General/mercurial.scala Sun May 29 17:37:43 2022 +0200
+++ b/src/Pure/General/mercurial.scala Sun May 29 20:57:10 2022 +0200
@@ -257,17 +257,27 @@
dry_run: Boolean = false,
clean: Boolean = false,
filter: List[String] = Nil,
+ rev: String = ""
): Unit = {
Isabelle_System.with_tmp_dir("rsync") { tmp_dir =>
- val exclude_path = tmp_dir + Path.explode("exclude")
- val exclude = status(options = "--unknown --ignored --no-status")
- File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
+ val (options, source) =
+ if (rev.isEmpty) {
+ val exclude_path = tmp_dir + Path.explode("exclude")
+ val exclude = status(options = "--unknown --ignored --no-status")
+ File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
- val options = List("--exclude-from=" + exclude_path.implode)
- val source = ssh.rsync_url + root.expand.implode + "/."
+ val options = List("--exclude-from=" + exclude_path.implode)
+ val source = ssh.rsync_url + root.expand.implode
+ (options, source)
+ }
+ else {
+ val source = File.standard_path(tmp_dir + Path.explode("archive"))
+ archive(source, rev = rev)
+ (Nil, source)
+ }
Isabelle_System.rsync(
progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, filter = filter,
- args = List("--prune-empty-dirs") ::: options ::: List("--", source, target)).check
+ args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target)).check
}
}
@@ -469,12 +479,13 @@
/** hg_sync **/
val isabelle_tool2 =
- Isabelle_Tool("hg_sync", "synchronize Mercurial repository working directory",
+ Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
Scala_Project.here, { args =>
var clean = false
var protect: List[String] = Nil
var root: Option[Path] = None
var dry_run = false
+ var rev = ""
var verbose = false
val getopts = Getopts("""
@@ -488,9 +499,10 @@
(default: implicit from current directory)
-f force changes: no dry-run
-n no changes: dry-run
+ -r REV explicit revision (default: state of working directory)
-v verbose
- Synchronize Mercurial repository working directory with other TARGET,
+ Synchronize Mercurial repository with TARGET directory,
which can be local or remote (using notation of rsync).
""",
"C" -> { _ => clean = true; dry_run = true },
@@ -498,6 +510,7 @@
"R:" -> (arg => root = Some(Path.explode(arg))),
"f" -> (_ => dry_run = false),
"n" -> (_ => dry_run = true),
+ "r:" -> (arg => rev = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -513,9 +526,8 @@
case Some(dir) => repository(dir)
case None => the_repository(Path.current)
}
- hg.sync(target, verbose = verbose, dry_run = dry_run, clean = clean,
- filter = protect.map("protect /" + _),
- progress = progress)
+ hg.sync(target, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
+ filter = protect.map("protect /" + _), rev = rev)
}
)
}