--- a/NEWS Sun May 29 15:16:49 2022 +0200
+++ b/NEWS Sun May 29 16:25:37 2022 +0200
@@ -117,6 +117,10 @@
explicitly. This increases the chances that the Java/Scala IDE project
works properly.
+* Command-line tool "isabelle hg_sync" synchronizes the working
+directory of a local Mercurial repository with a target directory, using
+rsync notation for destinations.
+
New in Isabelle2021-1 (December 2021)
--- a/src/Doc/System/Misc.thy Sun May 29 15:16:49 2022 +0200
+++ b/src/Doc/System/Misc.thy Sun May 29 16:25:37 2022 +0200
@@ -300,6 +300,63 @@
\<close>
+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.
+
+ @{verbatim [display]
+\<open>Usage: isabelle hg_sync [OPTIONS] TARGET
+
+ Options are:
+ -C clean all unknown/ignored files on target
+ (implies -n for testing; use 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
+ -n no changes: dry-run
+ -v verbose
+
+ Synchronize Mercurial repository working directory with other TARGET,
+ 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>-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.
+
+ \<^medskip> Option \<^verbatim>\<open>-C\<close> causes deletion of all unknown/ignored files on the target.
+ This is potentially dangerous: giving a wrong target directory will cause
+ its total destruction! For robustness, option \<^verbatim>\<open>-C\<close> implies option \<^verbatim>\<open>-n\<close>,
+ for ``dry-run'' with verbose output. A subsequent option \<^verbatim>\<open>-f\<close> is required
+ to force actual deletions on the target.
+
+ \<^medskip> Option \<^verbatim>\<open>-P\<close> protects a given file or directory from deletion; multiple
+ \<^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.
+\<close>
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Synchronize the Isabelle repository onto a remote host, while
+ protecting a copy of AFP inside of it (without changing that):
+ @{verbatim [display] \<open> isabelle hg_sync -R '$ISABELLE_HOME' -P AFP -C testmachine:test/isabelle\<close>}
+
+ So far, this is only a dry run. In a realistic situation, it requires
+ consecutive options \<^verbatim>\<open>-C -f\<close> as confirmation.
+\<close>
+
+
section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close>
text \<open>
--- a/src/Pure/General/mercurial.scala Sun May 29 15:16:49 2022 +0200
+++ b/src/Pure/General/mercurial.scala Sun May 29 16:25:37 2022 +0200
@@ -480,7 +480,7 @@
Options are:
-C clean all unknown/ignored files on target
- (potentially DANGEROUS: use with option -f to confirm)
+ (implies -n for testing; use option -f to confirm)
-P NAME protect NAME within TARGET from deletion
-R ROOT explicit repository root directory
(default: implicit from current directory)