diff -r 3e61534e804e -r 1579a9160c7f src/Doc/System/Phabricator.thy
--- a/src/Doc/System/Phabricator.thy	Thu Nov 14 16:22:21 2019 +0100
+++ b/src/Doc/System/Phabricator.thy	Thu Nov 14 21:49:49 2019 +0100
@@ -23,15 +23,14 @@
   especially due to Microsoft's Github and Atlassian's Bitbucket.
 
   The small company behind Phabricator provides paid plans for support and
-  hosting of servers, but it is relatively easy to do \<^emph>\<open>independent
-  self-hosting\<close> on a standard LAMP server (Linux, Apache, MySQL, PHP). This
-  merely requires a virtual Ubuntu server on the net, which can be rented
-  rather cheaply from local hosting providers (there is no need to follow big
-  cloud corporations). So it is feasible to remain the master of your virtual
-  home, following the slogan ``own all your data''. In many respects,
-  Phabricator is similar to the well-known
-  Nextcloud\<^footnote>\<open>\<^url>\<open>https://nextcloud.com\<close>\<close> product, concerning both the
-  technology and sociology.
+  hosting of servers, but it is easy to do \<^emph>\<open>independent self-hosting\<close> on a
+  standard LAMP server (Linux, Apache, MySQL, PHP). This merely requires a
+  virtual machine on the Net, which can be rented cheaply from local hosting
+  providers --- there is no need to follow big cloud corporations. So it is
+  feasible to remain the master of your virtual home, following the slogan
+  ``own all your data''. In many respects, Phabricator is similar to the
+  well-known Nextcloud\<^footnote>\<open>\<^url>\<open>https://nextcloud.org\<close>\<close> product, concerning both
+  the technology and sociology.
 
   \<^medskip>
   The following Phabricator instances may serve as examples:
@@ -41,89 +40,94 @@
     \<^item> Mercurial development \<^url>\<open>https://phab.mercurial-scm.org\<close>
     \<^item> Isabelle development \<^url>\<open>https://isabelle-dev.sketis.net\<close>
 
-  \<^medskip> Initial Phabricator server configuration requires many details to be done
+  \<^medskip> Initial Phabricator configuration requires many details to be done
   right.\<^footnote>\<open>See also
   \<^url>\<open>https://secure.phabricator.com/book/phabricator/article/installation_guide\<close>
   in the context of \<^url>\<open>https://help.ubuntu.com/lts/serverguide\<close>.\<close> Isabelle
   provides some command-line tools to help with the setup, and afterwards
   Isabelle support is optional: it is possible to run and maintain the server,
-  without requiring a full Isabelle distribution again.
+  without requiring the somewhat bulky Isabelle distribution again.
 \<close>
 
 
 section \<open>Quick start\<close>
 
 text \<open>
-  The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04 LTS\<close>: that
-  particular version is required due to subtle dependencies on system
-  configuration and add-on packages.
+  The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04
+  LTS\<close>\<^footnote>\<open>\<^url>\<open>https://ubuntu.com/download\<close>\<close>: this version is mandatory due to
+  subtle dependencies on system packages and configuration that is assumed by
+  the Isabelle setup tool.
 
   For production use, a proper \<^emph>\<open>Virtual Server\<close> or \<^emph>\<open>Root Server\<close> product
   from a hosting provider will be required, including an Internet Domain Name
   (a pseudo sub-domain in the style of Apache is sufficient).
 
   Initial experimentation also works on a local host, e.g.\ via
-  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public server behind
-  \<^verbatim>\<open>lvh.me\<close> provides arbitrary subdomains as an alias to \<^verbatim>\<open>localhost\<close>, which
-  will be used for the default installation below.
+  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public domain \<^verbatim>\<open>lvh.me\<close> is
+  used below: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
 
   All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
-  \<^verbatim>\<open>sudo\<close>).
+  \<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the
+  user home directory via @{setting ISABELLE_HOME_USER}
+  (\secref{sec:settings}); that may be different or absent for the root user
+  and thus cause confusion.
 \<close>
 
 
 subsection \<open>Initial setup\<close>
 
 text \<open>
-  Isabelle can managed multiple named installations Phabricator installations:
-  this allows to separate administrative responsibilities, e.g.\ different
-  approaches to user management for different projects. Subsequently we always
-  use the implicit default name ``\<^verbatim>\<open>vcs\<close>'': it will appear in file and
-  directory locations, internal database names and URLs.
+  Isabelle can manage multiple named Phabricator installations: this allows to
+  separate administrative responsibilities, e.g.\ different approaches to user
+  management for different projects. Subsequently we always use the default
+  name ``\<^verbatim>\<open>vcs\<close>'': it will appear in file and directory locations, internal
+  database names and URLs.
 
-  The initial setup (with full Linux package upgrade) works as follows:
+  The initial setup works as follows (with full Linux package upgrade):
 
   @{verbatim [display] \<open>  isabelle phabricator_setup -U\<close>}
 
-  After installing many packages and cloning the Phabricator distribution, the
-  final output of the tool should be the URL for further manual configuration
-  (using a local web browser). Here the key points are:
+  After installing many packages, cloning the Phabricator distribution,
+  initializing the MySQL database and Apache, the tool prints an URL for
+  further configuration. The following needs to be provided by the web
+  interface:
 
-    \<^item> An initial user account that will get administrator rights. There is no
-    need to create a separate \<^verbatim>\<open>admin\<close> account. Instead, a regular user that
-    will take over this responsibility can be used here. Subsequently we
-    assume that user \<^verbatim>\<open>makarius\<close> becomes the initial administrator.
+    \<^item> An initial user that will get administrator rights. There is no need to
+    create a special \<^verbatim>\<open>admin\<close> account. Instead, a regular user that will take
+    over this responsibility can be used here. Subsequently we assume that
+    user \<^verbatim>\<open>makarius\<close> becomes the initial administrator.
 
     \<^item> An \<^emph>\<open>Auth Provider\<close> to manage user names and passwords. None is provided
     by default, and Phabricator points out this omission prominently in its
     overview of \<^emph>\<open>Setup Issues\<close>: following these hints quickly leads to the
     place where a regular \<^emph>\<open>Username/Password\<close> provider can be added.
 
-  Note that Phabricator allows to delegate the responsibility of
-  authentication to big corporations like Google and Facebook, but these can
-  be easily avoided. Genuine self-hosting means to manage users directly,
-  without outsourcing of authentication.
+    Alternatively, Phabricator can delegate the responsibility of
+    authentication to big corporations like Google and Facebook, but these can
+    be ignored. Genuine self-hosting means to manage users directly, without
+    outsourcing of authentication.
 
-  \<^medskip>
-  With the Auth Provider available, the administrator can now set a proper
-  password. This works e.g.\ by initiating a local password reset procedure:
+    \<^item> A proper password for the administrator can now be set, e.g.\ by the
+    following command:
 
-  @{verbatim [display] \<open>  isabelle phabricator bin/auth recover makarius\<close>}
+    @{verbatim [display] \<open>  isabelle phabricator bin/auth recover makarius\<close>}
 
-  The printed URL gives access to a password dialog in the web browser.
+    The printed URL gives access to a login and password dialog in the web
+    interface.
 
-  Further users will be able to provide a password more directly, because the
-  Auth Provider is now active.
+    Any further users will be able to provide a password directly, because the
+    Auth Provider is already active.
+
+    \<^item> The list of Phabricator \<^bold>\<open>Setup Issues\<close> should be studied with some
+    care, to make sure that no serious problems are remaining. The request to
+    lock the configuration can be fulfilled as follows:
 
-  \<^medskip>
-  The pending request in Phabricator \<^bold>\<open>Setup Issues\<close> to lock the configuration
-  can be fulfilled as follows:
+    @{verbatim [display] \<open>  isabelle phabricator bin/auth lock\<close>}
 
-  @{verbatim [display] \<open>  isabelle phabricator bin/auth lock\<close>}
-
-  \<^medskip>
-  Most other Setup Issues can be ignored, after reading through them briefly
-  to make sure that there are no genuine problems remaining.
+    \<^medskip> A few other Setup Issues might be relevant as well, e.g.\ the timezone
+    of the server. Some more exotic points can be ignored: Phabricator
+    provides careful explanations about what it thinks could be wrong, always
+    leaving some room for interpretation.
 \<close>
 
 
@@ -131,34 +135,38 @@
 
 text \<open>
   The next important thing is messaging: Phabricator needs to be able to
-  communicate with users. There are many variations on \<^emph>\<open>Mailer
-  Configuration\<close>, but a conventional SMTP server connection with a dedicated
-  \<^verbatim>\<open>phabricator\<close> user is sufficient. Note that there is no need to run a mail
-  server on the self-hosted Linux machine: regular web-hosting packages
-  usually allow to create new mail accounts easily. (As a last resort it is
-  possible to use a service like Gmail, but that would again introduce
-  unnecessary dependency on Google.)
+  communicate with users on its own account, e.g.\ to reset passwords. The
+  documentation has many variations on \<^emph>\<open>Configuring Outbound
+  Email\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email\<close>\<close>,
+  but a conventional SMTP server with a dedicated \<^verbatim>\<open>phabricator\<close> user is
+  sufficient. There is no need to run a separate mail server on the
+  self-hosted Linux machine: hosting providers often include such a service
+  for free, e.g.\ as part of a web-hosting package. As a last resort it is
+  also possible to use a corporate service like Gmail, but such dependency
+  dilutes the whole effort of self-hosting.
 
   \<^medskip>
   Mailer configuration requires a few command-line invocations as follows:
 
   @{verbatim [display] \<open>  isabelle phabricator_setup_mail\<close>}
 
-  \<^noindent> Now edit the generated JSON file to provide the mail account details. Then
-  add and test it with Phabricator like this (to let Phabricator send a
-  message to the administrator from above):
+  \<^noindent> This generates a JSON template file for the the mail account details.
+  After editing that, the subsequent command will add and test it with
+  Phabricator:
 
   @{verbatim [display] \<open>  isabelle phabricator_setup_mail -T makarius\<close>}
 
-  The mail configuration process can be refined and repeated until it really
-  works: host name, port number, protocol etc.\ all need to be correct. The
-  \<^verbatim>\<open>key\<close> field in the JSON file identifies the name of the configuration; it
+  This tells Phabricator to send a message to the administrator created
+  before; the output informs about success or errors.
+
+  The mail configuration process can be refined and repeated until it works
+  properly: host name, port number, protocol etc.\ all need to be correct. The
+  \<^verbatim>\<open>key\<close> field in the JSON file identifies the name of the configuration that
   will be overwritten each time, when taking over the parameters via
   \<^verbatim>\<open>isabelle phabricator_setup_mail\<close>.
 
   \<^medskip>
-  For information, the resulting mailer configuration can be queried like
-  this:
+  This is how to query the current mail configuration:
 
   @{verbatim [display] \<open>  isabelle phabricator bin/config get cluster.mailers\<close>}
 \<close>
@@ -169,10 +177,7 @@
 text \<open>
   The subsequent command-line tools usually require root user privileges on
   the underlying Linux system (e.g.\ via \<^verbatim>\<open>sudo bash\<close> to open a subshell, or
-  directly via \<^verbatim>\<open>sudo isabelle ...\<close>). Note that Isabelle refers to
-  user-specific configuration in the user home directory via @{setting
-  ISABELLE_HOME_USER} (\secref{sec:settings}); that may be different or absent
-  for the root user and thus cause confusion.
+  directly via \<^verbatim>\<open>sudo isabelle phabricator ...\<close>).
 \<close>
 
 
@@ -217,8 +222,8 @@
   @{verbatim [display] \<open>phabricator/ $ ./bin/config get phabricator.base-uri\<close>}
 
   Here the user is meant to navigate to the Phabricator home manually, in
-  contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically based on
-  \<^path>\<open>/etc/isabelle-phabricator.conf\<close>.
+  contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically thanks to the
+  global configuration \<^path>\<open>/etc/isabelle-phabricator.conf\<close>.
 \<close>
 
 
@@ -226,7 +231,7 @@
 
 text \<open>
   The @{tool_def phabricator_setup} installs a fresh Phabricator instance on
-  Ubuntu Linux (notably 18.04 LTS):
+  Ubuntu 18.04 LTS:
   @{verbatim [display] \<open>Usage: isabelle phabricator_setup [OPTIONS]
 
   Options are:
@@ -240,41 +245,40 @@
   The installation name (default: "vcs") is mapped to a regular
   Unix user; this is relevant for public SSH access.\<close>}
 
-  Installation requires Linux root user access. All required packages are
+  Installation requires Linux root permissions. All required packages are
   installed automatically beforehand, this includes the Apache web server and
   the MySQL database engine.
 
-  Global configuration in \<^verbatim>\<open>/etc\<close> and other directories like \<^verbatim>\<open>/var/www\<close>
-  always use name prefixes \<^verbatim>\<open>isabelle-phabricator\<close> or \<^verbatim>\<open>phabricator\<close>. Local
+  Global configuration in \<^verbatim>\<open>/etc\<close> or a few other directories like \<^verbatim>\<open>/var/www\<close>
+  uses name prefixes like \<^verbatim>\<open>isabelle-phabricator\<close> or \<^verbatim>\<open>phabricator\<close>. Local
   configuration for a particular installation uses more specific names derived
-  from \<^verbatim>\<open>phabricator-\<close>\<open>NAME\<close>, e.g. \<^verbatim>\<open>/var/www/phabricator-vcs\<close> for a default
-  installation.
+  from \<^verbatim>\<open>phabricator-\<close>\<open>NAME\<close>, e.g.\ \<^verbatim>\<open>/var/www/phabricator-vcs\<close> for the
+  default.
 
-  Knowing the conventions, it is possible to purge a Linux installation from
-  Isabelle/Phabricator with some effort. There is no automated
-  de-installation: it is often better to re-install a clean virtual machine
-  image.
+  Knowing the naming conventions, it is possible to purge a Linux installation
+  from Isabelle/Phabricator with some effort, but there is no automated
+  procedure for de-installation. In the worst case, it might be better to
+  re-install the virtual machine from a clean image.
 
   \<^medskip>
   Option \<^verbatim>\<open>-U\<close> ensures a full update of system packages, before installing
-  further packages required by Phabricator.
+  further packages required by Phabricator. This might require to reboot.
 
   Option \<^verbatim>\<open>-n\<close> provides an alternative installation name. The default name
-  \<^verbatim>\<open>vcs\<close> means ``Version Control System''. The name will appear in the URL for
-  SSH access, and thus has some relevance to end-users. The initial server URL
-  also uses that name suffix, but it can be changed later via regular Apache
-  configuration.
+  \<^verbatim>\<open>vcs\<close> means ``version control system''. The name appears in the URL for SSH
+  access, and thus has some relevance to end-users. The initial server URL
+  also uses the same suffix, but that can (and should) be changed later via
+  regular Apache configuration.
 
   Option \<^verbatim>\<open>-r\<close> specifies an alternative installation root directory: it needs
   to be accessible for the Apache web server.
 
   Option \<^verbatim>\<open>-R\<close> specifies an alternative directory for repositories that are
   hosted by Phabricator. Provided that it is accessible for the Apache web
-  server, the directory can be re-used directly for the builtin \<^verbatim>\<open>hgweb\<close> view
-  by Mercurial. See also the documentation
-  \<^url>\<open>https://www.mercurial-scm.org/wiki/PublishingRepositories#hgweb\<close> and the
-  example \<^url>\<open>https://isabelle.sketis.net/repos\<close> for repositories in
-  \<^url>\<open>https://isabelle-dev.sketis.net/diffusion\<close>.
+  server, the directory can be reused for the \<^verbatim>\<open>hgweb\<close> view by Mercurial.\<^footnote>\<open>See
+  also the documentation
+  \<^url>\<open>https://www.mercurial-scm.org/wiki/PublishingRepositories\<close> and the
+  example \<^url>\<open>https://isabelle.sketis.net/repos\<close>.\<close>
 \<close>
 
 
@@ -282,7 +286,7 @@
 
 text \<open>
   The @{tool_def phabricator_setup_mail} provides mail configuration for an
-  existing Phabricator installation (preferably via SMTP):
+  existing Phabricator installation:
   @{verbatim [display] \<open>Usage: isabelle phabricator_setup_mail [OPTIONS]
 
   Options are:
@@ -295,15 +299,15 @@
 
   Proper mail configuration is vital for Phabricator, but the details can be
   tricky. A common approach is to re-use an existing SMTP mail service, as is
-  often included in regular web hosting packages. A single account for
-  multiple Phabricator installations is sufficient, but the configuration
-  needs to be set for each installation separately.
+  often included in regular web hosting packages. It is sufficient to create
+  one mail account for multiple Phabricator installations, but the
+  configuration needs to be set for each installation.
 
   The first invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> without options
   creates a JSON template file. Its \<^verbatim>\<open>key\<close> entry should be changed to
   something sensible to identify the configuration, e.g.\ the Internet Domain
-  Name of the mail address being used here. The \<^verbatim>\<open>options\<close> specify the SMTP
-  server address and account information.
+  Name of the mail address. The \<^verbatim>\<open>options\<close> specify the SMTP server address and
+  account information.
 
   Another invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> with updated JSON
   file will change the underlying Phabricator installation. This can be done
@@ -314,8 +318,9 @@
   address is derived from the user profile.
 
   Option \<^verbatim>\<open>-f\<close> refers to an existing JSON configuration file, e.g.\ from a
-  different Phabricator installation: sharing mailers setup with the same mail
-  address works for outgoing mails; incoming mails are not strictly needed.
+  previous successful Phabricator installation: sharing mailers setup with the
+  same mail address is fine for outgoing mails; incoming mails are optional
+  and not configured here.
 \<close>
 
 end