--- a/src/Doc/System/Misc.thy Thu Dec 19 16:21:52 2019 +0100
+++ b/src/Doc/System/Misc.thy Thu Dec 19 16:49:29 2019 +0100
@@ -149,6 +149,38 @@
\<close>
+section \<open>Mercurial repository setup \label{sec:hg-setup}\<close>
+
+text \<open>
+ The @{tool_def hg_setup} tool simplifies the setup of Mercurial
+ repositories, with hosting via Phabricator (\chref{ch:phabricator}) or plain
+ SSH file-system access.
+
+ @{verbatim [display]
+\<open>Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
+
+ Options are:
+ -n NAME remote repository name (default: base name of LOCAL_DIR)
+ -p PATH Mercurial path name (default: "default")
+ -r assume that remote repository already exists
+
+ Setup a remote vs. local Mercurial repository: REMOTE either refers to a
+ Phabricator server "user@host" or SSH file server "ssh://user@host/path".\<close>}
+
+ The \<^verbatim>\<open>REMOTE\<close> repository specification \<^emph>\<open>excludes\<close> the actual repository
+ name: that is given by the base name of \<^verbatim>\<open>LOCAL_DIR\<close>, or via option \<^verbatim>\<open>-n\<close>.
+
+ By default, both sides of the repository are created on demand by default.
+ In contrast, option \<^verbatim>\<open>-r\<close> assumes that the remote repository already exists:
+ it avoids accidental creation of a persistent repository with unintended
+ name.
+
+ The local \<^verbatim>\<open>.hg/hgrc\<close> file is changed to refer to the remote repository,
+ usually via the symbolic path name ``\<^verbatim>\<open>default\<close>''; option \<^verbatim>\<open>-p\<close> allows to
+ provided a different name.
+\<close>
+
+
section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close>
text \<open>
--- a/src/Doc/System/Phabricator.thy Thu Dec 19 16:21:52 2019 +0100
+++ b/src/Doc/System/Phabricator.thy Thu Dec 19 16:49:29 2019 +0100
@@ -4,7 +4,7 @@
imports Base
begin
-chapter \<open>Phabricator server administration\<close>
+chapter \<open>Phabricator server setup \label{ch:phabricator}\<close>
text \<open>
Phabricator\<^footnote>\<open>\<^url>\<open>https://www.phacility.com/phabricator\<close>\<close> is an open-source
@@ -47,6 +47,14 @@
afterwards Isabelle support is optional: it is possible to run and maintain
the server, without requiring the somewhat bulky Isabelle distribution
again.
+
+ \<^medskip>
+ Assuming an existing Phabricator installation, the command-line tool @{tool
+ hg_setup} (\secref{sec:hg-setup}) helps to create new repositories or to
+ migrate old ones. In particular, this avoids the lengthy sequence of clicks
+ in Phabricator to make a new private repository with hosting on the server.
+ (Phabricator is a software project management platform, where initial
+ repository setup happens rarely in practice.)
\<close>
--- a/src/Pure/General/mercurial.scala Thu Dec 19 16:21:52 2019 +0100
+++ b/src/Pure/General/mercurial.scala Thu Dec 19 16:49:29 2019 +0100
@@ -305,10 +305,10 @@
var remote_exists = false
val getopts = Getopts("""
-Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL
+Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
Options are:
- -n NAME remote repository name (default: base name of LOCAL directory)
+ -n NAME remote repository name (default: base name of LOCAL_DIR)
-p PATH Mercurial path name (default: """ + quote(default_path_name) + """)
-r assume that remote repository already exists