src/Doc/System/Misc.thy

   Both variants require SSH access to the target server, via public key
   without password.
 \<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>
   By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are
   just run from their location within the distribution directory, probably