# HG changeset patch
# User wenzelm
# Date 1653834337 -7200
# Node ID 1148c190eb9ba573a1cc3f2590b3ea68c32ab592
# Parent  f1d204a4d7950b36ff53551e9d6dd716ffb41e0c
more documentation;

diff -r f1d204a4d795 -r 1148c190eb9b NEWS
--- 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)
diff -r f1d204a4d795 -r 1148c190eb9b src/Doc/System/Misc.thy
--- 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>
diff -r f1d204a4d795 -r 1148c190eb9b src/Pure/General/mercurial.scala
--- 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)