# HG changeset patch
# User wenzelm
# Date 1576770569 -3600
# Node ID 0256ce61f4053f98b635c3e249a6318bba009d81
# Parent  edf3210a61a2590e1ff091e3b02220a9a5895ab1
more documentation;

diff -r edf3210a61a2 -r 0256ce61f405 src/Doc/System/Misc.thy
--- 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>
diff -r edf3210a61a2 -r 0256ce61f405 src/Doc/System/Phabricator.thy
--- 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>
 
 
diff -r edf3210a61a2 -r 0256ce61f405 src/Pure/General/mercurial.scala
--- 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