# HG changeset patch
# User wenzelm
# Date 1521725252 -3600
# Node ID 7dc2046237708447c3bce706eed04487fc85e99a
# Parent  d13b2dd20f5ef7c658d5f75b0fb7870968ff0369
misc tuning and clarification;

diff -r d13b2dd20f5e -r 7dc204623770 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Wed Mar 21 21:50:28 2018 +0100
+++ b/src/Doc/System/Server.thy	Thu Mar 22 14:27:32 2018 +0100
@@ -76,28 +76,29 @@
 
   \<^medskip>
   Option \<^verbatim>\<open>-c\<close> connects the console in/out channels after the initial check
-  for a suitable server process. Note that the @{tool client} tool
-  (\secref{sec:tool-client}) provides a more convenient way to do this
-  interactively, together with command-line editor support.
-
-  \<^medskip>
-  Option \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
-  details.
-
-  \<^medskip>
-  Option \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a \<^verbatim>\<open>shutdown\<close>
-  command.
+  for a suitable server process. Also note that the @{tool client} tool
+  (\secref{sec:tool-client}) provides a command-line editor to interact with
+  the server.
 
   \<^medskip>
   Option \<^verbatim>\<open>-L\<close> specifies a log file for exceptional output of internal server
   and session operations.
+
+  \<^medskip>
+  Operation \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
+  details.
+
+  \<^medskip>
+  Operation \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a
+  \<^verbatim>\<open>shutdown\<close> command.
 \<close>
 
 
 subsection \<open>Client \label{sec:tool-client}\<close>
 
 text \<open>
-  The @{tool_def client} provides console interaction for Isabelle servers:
+  The @{tool_def client} tool provides console interaction for Isabelle
+  servers:
   @{verbatim [display]
 \<open>Usage: isabelle client [OPTIONS]
 
@@ -107,8 +108,8 @@
 
   Console interaction for Isabelle server (with line-editor).\<close>}
 
-  This is a convenient wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
-  experimentation, wrapped into @{setting ISABELLE_LINE_EDITOR} if available.
+  This is a wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
+  experimentation, which uses @{setting ISABELLE_LINE_EDITOR} if available.
   The server name is sufficient for identification, as the client can
   determine the connection details from the local database of active servers.
 
@@ -126,10 +127,9 @@
   Ensure that a particular server instance is running in the background:
   @{verbatim [display] \<open>isabelle server -n test &\<close>}
 
-  Here the first line of output presents the connection details:\<^footnote>\<open>This
-  information may be used in an independent TCP client, while the
-  Isabelle/Scala tool merely needs the server name to access the database of
-  servers.\<close>
+  The first line of output presents the connection details:\<^footnote>\<open>This information
+  may be used in other TCP clients, without access to Isabelle/Scala and the
+  underlying database of running servers.\<close>
   @{verbatim [display] \<open>server "test" = 127.0.0.1:4711 (password "XYZ")\<close>}
 
   \<^medskip>
@@ -152,7 +152,7 @@
   possible to reconnect again, and have multiple connections at the same time.
 
   \<^medskip>
-  Finally, exit the named server on the command-line:
+  Exit the named server on the command-line:
   @{verbatim [display] \<open>isabelle server -n test -x\<close>}
 \<close>
 
@@ -161,12 +161,12 @@
 
 text \<open>
   The Isabelle server listens on a regular TCP socket, using a line-oriented
-  protocol of structured messages: input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
+  protocol of structured messages. Input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
   (via \<^verbatim>\<open>OK\<close> or \<^verbatim>\<open>ERROR\<close>) are strictly alternating on the toplevel, but
   commands may also return a \<^emph>\<open>task\<close> identifier to indicate an ongoing
   asynchronous process that is joined later (via \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>).
   Asynchronous \<^verbatim>\<open>NOTE\<close> messages may occur at any time: they are independent of
-  the main command-reply protocol.
+  the main command-result protocol.
 
   For example, the synchronous \<^verbatim>\<open>echo\<close> command immediately returns its
   argument as \<^verbatim>\<open>OK\<close> result. In contrast, the asynchronous \<^verbatim>\<open>session_build\<close>
@@ -176,7 +176,7 @@
   may emit asynchronous messages of the form \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>
   to inform about its progress. Due to the explicit task identifier, the
   client can show these messages in the proper context, e.g.\ a GUI window for
-  the session build job.
+  this particular session build job.
 
   \medskip Subsequently, the protocol message formats are described in further
   detail.
@@ -191,22 +191,22 @@
   particular length. Messages are written as a single chunk that is flushed
   immediately.
 
-  The message boundary is determined as follows:
+  Message boundaries are determined as follows:
 
     \<^item> A \<^emph>\<open>short message\<close> consists of a single line: it is a sequence of
     arbitrary bytes excluding CR (13) and LF (10), and terminated by CR-LF or
     just LF.
 
-    \<^item> A \<^emph>\<open>long message\<close> starts with a single line as above, which consists
-    only of decimal digits: that is interpreted as length of the subsequent
-    block of arbitrary bytes. A final line-terminator may be included here,
+    \<^item> A \<^emph>\<open>long message\<close> starts with a single that consists only of decimal
+    digits: these are interpreted as length of the subsequent block of
+    arbitrary bytes. A final line-terminator (as above) may be included here,
     but is not required.
 
   Messages in JSON format (see below) always fit on a single line, due to
   escaping of newline characters within string literals. This is convenient
   for interactive experimentation, but it can impact performance for very long
   messages. If the message byte-length is given on the preceding line, the
-  server can read the message efficiently as a single block.
+  server can read the message more efficiently as a single block.
 \<close>
 
 
@@ -232,13 +232,13 @@
     \<^item> \<open>name argument\<close> such that:
 
     \<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
-    ``\<^verbatim>\<open>_\<close>'' (underscore), or ``\<^verbatim>\<open>.\<close>'' (dot),
+    ``\<^verbatim>\<open>_\<close>'', ``\<^verbatim>\<open>.\<close>'',
 
     \<^item> the separator between \<open>name\<close> and \<open>argument\<close> is the longest possible
     sequence of ASCII blanks (it could be empty, e.g.\ when the argument
     starts with a quote or bracket),
 
-    \<^item> \<open>argument\<close> is the rest of the message without the line terminator.
+    \<^item> \<open>argument\<close> is the rest of the message without line terminator.
 
   \<^medskip>
   Input messages are sent from the client to the server. Here the \<open>name\<close>
@@ -283,7 +283,8 @@
   Whenever a new client opens the server socket, the initial message needs to
   be its unique password. The server replies either with \<^verbatim>\<open>OK\<close> (and some
   information about the Isabelle version) or by silent disconnection of what
-  is considered an illegal connection attempt.
+  is considered an illegal connection attempt. Note that @{tool client}
+  already presents the correct password internally.
 
   Server passwords are created as Universally Unique Identifier (UUID) in
   Isabelle/Scala and stored in a per-user database, with restricted
@@ -301,7 +302,7 @@
   Isabelle/Scala, with single argument and result (regular or error). Both the
   argument and the result may consist of type \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close>.
   An error result typically consists of a JSON object with error message and
-  potentially further fields (this resembles exceptions in Scala).
+  potentially further result fields (this resembles exceptions in Scala).
 
   These are the protocol exchanges for both cases of command execution:
   \begin{center}
@@ -318,11 +319,11 @@
 
 text \<open>
   An \<^emph>\<open>asynchronous command\<close> corresponds to an ongoing process that finishes
-  or fails eventually, while emitting arbitrary notifications intermediately.
-  Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close> and
-  the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad command
-  syntax. For a running task, the termination is indicated later by
-  \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result.
+  or fails eventually, while emitting arbitrary notifications in between.
+  Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close>
+  giving the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad
+  command syntax. For a running task, the termination is indicated later by
+  \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result value.
 
   These are the protocol exchanges for various cases of command task
   execution:
@@ -332,7 +333,6 @@
   \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> \\
   intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
-  intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   (a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   (b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FAILED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\[3ex]
   \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
@@ -341,34 +341,18 @@
   \end{center}
 
   All asynchronous messages are decorated with the task identifier that was
-  revealed in the immediate (synchronous) result. Thus it is possible to emit
-  further asynchronous commands and dispatch the mingled stream of
+  revealed in the immediate (synchronous) result. Thus the client can
+  invoke further asynchronous commands and still dispatch the resulting stream of
   asynchronous messages properly.
 
   The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
   prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is not guaranteed:
-  the cancel event may come too late or the task may just ignore it.
+  the cancel event may come too late or the running process may just ignore
+  it.
 \<close>
 
 
-section \<open>Server commands and results\<close>
-
-text \<open>
-  Here follows an overview of particular Isabelle server commands with their
-  results, which are usually represented as JSON values. The general format of
-  input and output messages is described in
-  \secref{sec:input-output-messages}. The relevant Isabelle/Scala source files
-  are:
-
-  \<^medskip>
-  \begin{tabular}{l}
-  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
-  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close>
-  \end{tabular}
-\<close>
-
-
-subsection \<open>Types for JSON values\<close>
+section \<open>Types for JSON values \label{sec:json-types}\<close>
 
 text \<open>
   In order to specify concrete JSON types for command arguments and result
@@ -381,24 +365,25 @@
       'bool' | 'int' | 'long' | 'double' | 'string' | '[' @{syntax type} ']' |
       '{' (@{syntax field_type} ',' *) '}' |
       @{syntax type} '\<oplus>' @{syntax type} |
-      @{syntax type} '|' @{syntax type}
+      @{syntax type} '|' @{syntax type} |
+      '(' @{syntax type} ')'
     ;
     @{syntax field_type}: @{syntax name} ('?'?) ':' @{syntax type}
   \<close>
 
-  This is a simplified version of interfaces in
-  TypeScript.\<^footnote>\<open>\<^url>\<open>https://www.typescriptlang.org/docs/handbook/interfaces.html\<close>\<close>
-  The meaning of these types is specified wrt. the implementation in
-  Isabelle/Scala as follows.
+  This is a simplified variation of TypeScript
+  interfaces.\<^footnote>\<open>\<^url>\<open>https://www.typescriptlang.org/docs/handbook/interfaces.html\<close>\<close>
+  The meaning of these types is specified wrt. the Isabelle/Scala
+  implementation as follows.
 
   \<^item> A \<open>name\<close> refers to a type defined elsewhere. The environment of type
   definitions is given informally: put into proper foundational order, it
-  needs to specify a strongly normalizing system; type definitions may not be
-  recursive.
+  needs to specify a strongly normalizing system of syntactic abbreviations;
+  type definitions may not be recursive.
 
   \<^item> A \<open>value\<close> in JSON notation represents the singleton type of the given
-  item. For example, the string \<^verbatim>\<open>"error"\<close> can be used is the type for a slot
-  that is guaranteed to contain that constant.
+  item. For example, the string \<^verbatim>\<open>"error"\<close> can be used as type for a slot that
+  is guaranteed to contain that constant.
 
   \<^item> Type \<open>any\<close> is the super type of all other types: it is an untyped slot in
   the specification and corresponds to \<^verbatim>\<open>Any\<close> or \<^verbatim>\<open>JSON.T\<close> in Isabelle/Scala.
@@ -408,7 +393,7 @@
   ``Null References: The Billion Dollar Mistake'' by Tony Hoare
   \<^url>\<open>https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare\<close>.\<close>
 
-  \<^item> Type \<open>bool\<close> is the type of the truth values \<open>true\<close> and \<open>false\<close>; it
+  \<^item> Type \<open>bool\<close> is the type of the truth values \<^verbatim>\<open>true\<close> and \<^verbatim>\<open>false\<close>; it
   corresponds to \<^verbatim>\<open>Boolean\<close> in Scala.
 
   \<^item> Types \<open>int\<close>, \<open>long\<close>, \<open>double\<close> are specific versions of the generic
@@ -422,18 +407,18 @@
 
   \<^item> Type \<open>[t]\<close> is the array (or list) type over \<open>t\<close>; it corresponds to
   \<^verbatim>\<open>List[t]\<close> in Scala. The list type is co-variant as usual (i.e.\ monotonic
-  wrt. the subtype order).
+  wrt. the subtype relation).
 
   \<^item> Object types describe the possible content of JSON records, with field
   names and types. A question mark after a field name means that it is
-  optional: in Scala this could refer to an explicit type \<^verbatim>\<open>Option[t]\<close>. For
-  example, \<open>{a: int, b?: string}\<close> corresponds to a Scala case class with
-  arguments \<^verbatim>\<open>a: Int\<close>, \<^verbatim>\<open>b: Option[String]\<close>.
+  optional. In Scala this could refer to an explicit type \<^verbatim>\<open>Option[t]\<close>, e.g.\
+  \<open>{a: int, b?: string}\<close> corresponding to a Scala case class with arguments
+  \<^verbatim>\<open>a: Int\<close>, \<^verbatim>\<open>b: Option[String]\<close>.
 
   Alternatively, optional fields can have a default value. If nothing else is
-  specified, the standard default value is the ``empty'' value of a type,
-  i.e.\ \<^verbatim>\<open>0\<close> for the number types, \<^verbatim>\<open>false\<close> for \<open>bool\<close>, or the empty string,
-  array, object etc.
+  specified, a standard ``empty value'' is used for each type, i.e.\ \<^verbatim>\<open>0\<close> for
+  the number types, \<^verbatim>\<open>false\<close> for \<open>bool\<close>, or the empty string, array, object
+  etc.
 
   Object types are \<^emph>\<open>permissive\<close> in the sense that only the specified field
   names need to conform to the given types, but unspecified fields may be
@@ -447,18 +432,20 @@
   \<^item> The type expression \<open>t\<^sub>1 | t\<^sub>2\<close> is the disjoint union of two types, either
   one of the two cases may occur.
 
+  \<^item> Parentheses \<open>(t)\<close> merely group type expressions syntactically.
+
 
   These types correspond to JSON values in an obvious manner, which is not
   further described here. For example, the JSON array \<^verbatim>\<open>[1, 2, 3]\<close> conforms to
   types \<open>[int]\<close>, \<open>[long]\<close>, \<open>[double]\<close>, \<open>[any]\<close>, \<open>any\<close>.
 
   Note that JSON objects require field names to be quoted, but the type
-  language omits quotes for clarity. Thus \<^verbatim>\<open>{"a": 42, "b": "xyz"}\<close> conforms to
-  the type \<open>{a: int, b: string}\<close>, for example.
+  language omits quotes for clarity. Thus the object \<^verbatim>\<open>{"a": 42, "b": "xyz"}\<close>
+  conforms to the type \<open>{a: int, b: string}\<close>, for example.
 
   \<^medskip>
-  The absence of an argument or result is represented by type \<^verbatim>\<open>Unit\<close> in
-  Isabelle/Scala: it is written as empty text in the message \<open>argument\<close>
+  The absence of an argument or result is represented by the Scala type
+  \<^verbatim>\<open>Unit\<close>: it is written as empty text in the message \<open>argument\<close>
   (\secref{sec:input-output-messages}). This is not part of the JSON language.
 
   Server replies have name tags like \<^verbatim>\<open>OK\<close>, \<^verbatim>\<open>ERROR\<close>: these are used literally
@@ -467,16 +454,17 @@
   list (JSON array) of strings.
 
   \<^bigskip>
-  Here are some common type definitions, for use in the subsequent
-  specifications of command arguments and results.
+  Here are some common type definitions, for use in particular specifications
+  of command arguments and results.
 
   \<^item> \<^bold>\<open>type\<close>~\<open>position = {line?: int, offset?: int, end_offset?: int, file?:
-  string, id?: long}\<close> describes a source position within Isabelle source text.
-  Only the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
+  string, id?: long}\<close> describes a source position within Isabelle text. Only
+  the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
   Detailed \<open>offset\<close> and \<open>end_offset\<close> positions are counted according to
   Isabelle symbols, see @{ML_type Symbol.symbol} in Isabelle/ML @{cite
-  "isabelle-implementation"}. The position \<open>id\<close> belongs to the internal
-  representation of command transactions in the Isabelle/PIDE protocol.
+  "isabelle-implementation"}. The position \<open>id\<close> belongs to the representation
+  of command transactions in the Isabelle/PIDE protocol: it normally does not
+  occur in externalized positions.
 
   \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
   the \<open>kind\<close> provides some hint about the role and importance of the message.
@@ -492,9 +480,9 @@
   \<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
   string, session: string}\<close> reports formal progress in loading theories (e.g.\
   when building a session image). Apart from a regular output message, it also
-  reveals the formal theory name (e.g.\ \<^verbatim>\<open>HOL.Nat\<close>) and session name (e.g.\
-  \<^verbatim>\<open>HOL\<close>). Note that some rare theory names lack a proper session prefix, e.g.
-  theory \<^verbatim>\<open>Main\<close> in session \<^verbatim>\<open>HOL\<close>.
+  reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
+  \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
+  e.g. theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
 
   \<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
   common Isabelle timing information in seconds, usually with a precision of
@@ -506,7 +494,7 @@
   identifiers are created as private random numbers of the server and only
   revealed to the client that creates a certain resource (e.g.\ task or
   session). A client may disclose this information for use in a different
-  client connection: e.g.\ this allows to share sessions between multiple
+  client connection: this allows to share sessions between multiple
   connections.
 
   Client commands need to provide syntactically wellformed UUIDs: this is
@@ -515,8 +503,34 @@
 
   \<^item> \<^bold>\<open>type\<close>~\<open>task = {task: uuid}\<close> identifies a newly created asynchronous task
   and thus allows the client to control it by the \<^verbatim>\<open>cancel\<close> command. The same
-  task identification is included in messages and the final result produced by
-  this task.
+  task identification is included in all messages produced by this task.
+
+  \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
+  int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
+  represents a formal theory node status of the PIDE document model. Fields
+  \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close> account
+  for individual commands within a theory node; \<open>ok\<close> is an abstraction for
+  \<open>failed = 0\<close>. The \<open>consolidated\<close> flag indicates whether the outermost theory
+  command structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has
+  been checked.
+\<close>
+
+
+section \<open>Server commands and results\<close>
+
+text \<open>
+  Here follows an overview of particular Isabelle server commands with their
+  results, which are usually represented as JSON values with types according
+  to \secref{sec:json-types}. The general format of input and output messages
+  is described in \secref{sec:input-output-messages}. The relevant
+  Isabelle/Scala source files are:
+
+  \<^medskip>
+  \begin{tabular}{l}
+  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
+  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close> \\
+  \<^file>\<open>$ISABELLE_HOME/src/Pure/General/json.scala\<close> \\
+  \end{tabular}
 \<close>
 
 
@@ -528,9 +542,9 @@
   \end{tabular}
   \<^medskip>
 
-  The \<^verbatim>\<open>help\<close> command has no argument and returns the list of command names
-  known to the server. This is occasionally useful for interactive
-  experimentation (see also @{tool client} in \secref{sec:tool-client}).
+  The \<^verbatim>\<open>help\<close> command has no argument and returns the list of server command
+  names. This is occasionally useful for interactive experimentation (see also
+  @{tool client} in \secref{sec:tool-client}).
 \<close>
 
 
@@ -547,8 +561,8 @@
   regular result. This is occasionally useful for testing and interactive
   experimentation (see also @{tool client} in \secref{sec:tool-client}).
 
-  The type of \<^verbatim>\<open>echo\<close> is actually more general than given above: \<^verbatim>\<open>Unit\<close>,
-  \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close> are supported uniformly. Note that \<^verbatim>\<open>XML.Elem\<close> might
+  The Scala type of \<^verbatim>\<open>echo\<close> is actually more general than given above:
+  \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close> work uniformly. Note that \<^verbatim>\<open>XML.Elem\<close> might
   be difficult to type on the console in its YXML syntax
   (\secref{sec:yxml-vs-xml}).
 \<close>
@@ -568,9 +582,8 @@
   connections!
 
   \<^medskip>
-  Likewise, the command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server
-  connection and issues a \<^verbatim>\<open>shutdown\<close> command (see also
-  \secref{sec:tool-server}).
+  The command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server connection
+  and issues a \<^verbatim>\<open>shutdown\<close> command (see also \secref{sec:tool-server}).
 \<close>
 
 
@@ -583,17 +596,17 @@
   \end{tabular}
   \<^medskip>
 
-  The command invocation \<^verbatim>\<open>cancel "\<close>\<open>id\<close>\<^verbatim>\<open>"\<close> attempts to cancel the specified
-  task.
+  The command invocation \<^verbatim>\<open>cancel "\<close>\<open>uuid\<close>\<^verbatim>\<open>"\<close> attempts to cancel the
+  specified task.
 
   Cancellation is merely a hint that the client prefers an ongoing process to
   be stopped. The command always succeeds formally, but it may get ignored by
-  a task that is still running, or it might refer to a non-existing or
-  no-longer existing task without producing an error.
+  a task that is still running; it might also refer to a non-existing or
+  no-longer existing task (without producing an error).
 
   Successful cancellation typically leads to an asynchronous failure of type
-  \<^verbatim>\<open>FAILED {\<close>\<open>task: string, message: \<close>\<^verbatim>\<open>"Interrupt"}\<close> --- or a slightly
-  different message, depending how the task handles the event.
+  \<^verbatim>\<open>FAILED {\<close>\<open>task: uuid, message:\<close>~\<^verbatim>\<open>"Interrupt"}\<close>. A different message is
+  also possible, depending how the task handles the event.
 \<close>
 
 
@@ -621,43 +634,45 @@
   \quad~~\<open>system_mode?: bool,\<close> \\
   \quad~~\<open>verbose?: bool}\<close> \\[2ex]
 
-  \<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
-  \quad\<open>{ok: bool,\<close> \\
-  \quad~~\<open>return_code: int,\<close> \\
-  \quad~~\<open>sessions: [session_build_result]}\<close> \\[2ex]
-
   \<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
   \quad\<open>{session: string,\<close> \\
   \quad~~\<open>ok: bool,\<close> \\
   \quad~~\<open>return_code: int,\<close> \\
   \quad~~\<open>timeout: bool,\<close> \\
-  \quad~~\<open>timing: timing}\<close> \\
+  \quad~~\<open>timing: timing}\<close> \\[2ex]
+
+  \<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
+  \quad\<open>{ok: bool,\<close> \\
+  \quad~~\<open>return_code: int,\<close> \\
+  \quad~~\<open>sessions: [session_build_result]}\<close> \\
   \end{tabular}
 \<close>
 
 text \<open>
-  The \<^verbatim>\<open>session_build\<close> command prepares given a session image for interactive
-  use of theories. This is a limited version of command-line tool @{tool
-  build} (\secref{sec:tool-build}), with specific options to request a formal
-  context of an interactive session: it also resembles options of @{tool
-  jedit} @{cite "isabelle-jedit"}.
+  The \<^verbatim>\<open>session_build\<close> command prepares a session image for interactive use of
+  theories. This is a limited version of command-line tool @{tool build}
+  (\secref{sec:tool-build}), with specific options to request a formal context
+  for an interactive PIDE session.
 
   The build process is asynchronous, with notifications that inform about the
-  progress of loaded theories. Some further human-readable messages may be
-  output as well.
+  progress of loaded theories. Some further informative messages are output as
+  well.
 
   Coordination of independent build processes is at the discretion of the
-  client: as for like @{tool build} there are no built-in measures against
-  conflicting builds with overlapping hierarchies of session images.
+  client (or end-user), just as for @{tool build} and @{tool jedit}. There is
+  no built-in coordination of conflicting builds with overlapping hierarchies
+  of session images. In the worst case, a session image produced by one task
+  may get overwritten by another task!
 \<close>
 
 
 subsubsection \<open>Arguments\<close>
 
 text \<open>
-  The field \<open>session\<close> is mandatory. It specifies the target session name:
-  either directly (default) or indirectly (if \<open>required_session\<close> is
-  \<^verbatim>\<open>true\<close>).
+  The \<open>session\<close> field is mandatory. It specifies the target session name:
+  either directly (default) or indirectly (if \<open>required_session\<close> is \<^verbatim>\<open>true\<close>).
+  The build process will produce all required ancestor images for the
+  specified target.
 
   \<^medskip>
   The environment of Isabelle system options is determined from \<open>preferences\<close>
@@ -671,9 +686,9 @@
   operating-system contexts.
 
   \<^medskip>
-  The \<open>dirs\<close> field specifies additional directories for session ROOT files
-  (\secref{sec:session-root}). This augments the name space of available
-  sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build} or @{tool jedit}.
+  The \<open>dirs\<close> field specifies additional directories for session ROOT and ROOTS
+  files (\secref{sec:session-root}). This augments the name space of available
+  sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
 
   \<^medskip>
   The \<open>ancestor_session\<close> field specifies an alternative image as starting
@@ -683,18 +698,18 @@
   session images of the hierarchy that are not used later on.
 
   \<^medskip>
-  The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all existing sessions from
-  reachable ROOT entries in the name space of theories with a proper
-  session-qualified name (instead of referring to the file-system location).
-  This could be relevant for the \<^verbatim>\<open>use_theories\<close> command
+  The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all sessions from reachable
+  ROOT entries into the name space of theories. This is relevant for proper
+  session-qualified names, instead of referring to theory file names. The
+  option enables the \<^verbatim>\<open>use_theories\<close> command
   (\secref{sec:command-use-theories}) to refer to arbitrary theories from
-  other sessions. Note that considerable time is required to explore all
-  accessible session directories and theory dependencies.
+  other sessions, but considerable time is required to explore all accessible
+  session directories and theory dependencies.
 
   \<^medskip>
-  The \<open>focus_session\<close> field set to \<^verbatim>\<open>true\<close> to focuses on the target session:
+  The \<open>focus_session\<close> field set to \<^verbatim>\<open>true\<close> focuses on the target session:
   the accessible name space of theories is restricted to sessions that are
-  connected to it.
+  connected to it in the imports graph.
 
   \<^medskip>
   The \<open>required_session\<close> field set to \<^verbatim>\<open>true\<close> indicates that the target image
@@ -703,14 +718,13 @@
   the \<open>session\<close> itself can be loaded.
 
   \<^medskip>
-  The \<open>system_mode\<close> field may be set to \<^verbatim>\<open>true\<close> to store session images and
+  The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
   log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
   @{setting ISABELLE_OUTPUT} (which is normally in @{setting
-  ISABELLE_HOME_USER}, i.e.\ the user's home directory). See also option \<^verbatim>\<open>-s\<close>
-  in @{tool build} and @{tool jedit}.
+  ISABELLE_HOME_USER}). See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
 
   \<^medskip>
-  The \<open>verbose\<close> field may be set to \<^verbatim>\<open>true\<close> for extra verbosity. The effect is
+  The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
   similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
 \<close>
 
@@ -723,28 +737,29 @@
   Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
 
   For the client it is usually sufficient to print the messages in plain text,
-  but note that \<open>theory_progress\<close> also reveals the internal \<open>theory\<close> and
-  \<open>session\<close> names.
+  but note that \<open>theory_progress\<close> also reveals formal \<open>theory\<close> and
+  \<open>session\<close> names directly.
 \<close>
 
 
 subsubsection \<open>Results\<close>
 
 text \<open>
-  The overall \<open>session_build_results\<close> contain both a summary and and entry
-  \<open>session_build_result\<close> for each session in the build hierarchy, leading up
-  to the specified target session. The result is always provided,
-  independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or failure (\<^verbatim>\<open>FAILED\<close>
-  task).
+  The overall \<open>session_build_results\<close> contain both a summary and an entry
+  \<open>session_build_result\<close> for each session in the build hierarchy. The result
+  is always provided, independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or
+  failure (\<^verbatim>\<open>FAILED\<close> task).
 
   The \<open>ok\<close> field tells abstractly, whether all required session builds came
-  out as \<open>ok\<close>, i.e.\ \<open>return_code\<close>. A non-zero \<open>return_code\<close> indicates an
-  error according to usual POSIX conventions for process exit.
+  out as \<open>ok\<close>, i.e.\ with zero \<open>return_code\<close>. A non-zero \<open>return_code\<close>
+  indicates an error according to usual POSIX conventions for process exit.
+
+  The individual \<open>session_build_result\<close> entries provide extra fields:
 
-  For individual \<open>session_build_result\<close> entries, there are additional fields:
-  \<open>timeout\<close> to tell if the build process was aborted after running too long,
-  and \<open>timing\<close> for the overall process timing in the usual Isabelle format
-  with elapsed, CPU, gc time.
+  \<^item> \<open>timeout\<close> tells if the build process was aborted after running too long,
+
+  \<^item> \<open>timing\<close> gives the overall process timing in the usual Isabelle format
+  with elapsed, CPU, GC time.
 \<close>
 
 
@@ -780,25 +795,25 @@
   \<^medskip>
   The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with
   underlying Isabelle/ML process, based on a session image that it produces on
-  demand in the same manner as \<^verbatim>\<open>session_build\<close>. Thus it accepts all
-  \<open>session_build_args\<close> and produces similar notifications, but the detailed
-  \<open>session_build_results\<close> are omitted.
+  demand using \<^verbatim>\<open>session_build\<close>. Thus it accepts all \<open>session_build_args\<close> and
+  produces similar notifications, but the detailed \<open>session_build_results\<close> are
+  omitted.
 
   The session build and startup process is asynchronous: when the task is
-  finished, the session remains active for commands such as \<^verbatim>\<open>use_theories\<close>
-  (\secref{sec:command-use-theories}), until a \<^verbatim>\<open>session_stop\<close> or \<^verbatim>\<open>shutdown\<close>
-  command is sent to the server.
+  finished, the session remains active for commands, until a \<^verbatim>\<open>session_stop\<close>
+  or \<^verbatim>\<open>shutdown\<close> command is sent to the server.
 
   Sessions are independent of client connections: it is possible to start a
   session and later apply \<^verbatim>\<open>use_theories\<close> on different connections, as long as
-  the internal session identifier is known.
+  the internal session identifier is known: shared theory imports will be used
+  only once (and persist until purged explicitly).
 \<close>
 
 
 subsubsection \<open>Arguments\<close>
 
 text \<open>
-  Most of the arguments are the same as for \<^verbatim>\<open>session_build\<close>
+  Most arguments are shared with \<^verbatim>\<open>session_build\<close>
   (\secref{sec:command-session-build}).
 
   \<^medskip>
@@ -826,6 +841,9 @@
 text \<open>
   Start a default Isabelle/HOL session:
   @{verbatim [display] \<open>session_start {"session": "HOL"}\<close>}
+
+  Start a session from the Archive of Formal Proofs:
+  @{verbatim [display] \<open>session_start {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
 \<close>
 
 
@@ -844,9 +862,9 @@
   \end{tabular}
 
   \<^medskip>
-  The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified
-  Isabelle/PIDE session. This asynchronous tasks usually finishes quickly.
-  Failure only happens unusual situations, according to the return code of the
+  The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified PIDE
+  session. This asynchronous tasks usually finishes quickly. Failure only
+  happens in unusual situations, according to the return code of the
   underlying Isabelle/ML process.
 \<close>
 
@@ -854,17 +872,19 @@
 subsubsection \<open>Arguments\<close>
 
 text \<open>
-  The \<open>session_id\<close> field is the UUID originally created by the server for the
-  intended session.
+  The \<open>session_id\<close> field provides the UUID originally created by the server
+  for this session.
 \<close>
 
 
 subsubsection \<open>Results\<close>
 
 text \<open>
-  The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process terminated
-  properly. The \<open>return_code\<close> expresses this information according to usual
-  POSIX conventions for process exit.
+  The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process has
+  terminated properly.
+
+  The \<open>return_code\<close> field expresses this information according to usual POSIX
+  conventions for process exit.
 \<close>
 
 
@@ -888,17 +908,9 @@
   \quad~~\<open>master_dir?: string,\<close> \\
   \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
+  \end{tabular}
 
-  \<^bold>\<open>type\<close> \<open>node_status =\<close> \\
-  \quad\<open>{ok: bool,\<close> \\
-  \quad~~\<open>total: int,\<close> \\
-  \quad~~\<open>unprocessed: int,\<close> \\
-  \quad~~\<open>running: int,\<close> \\
-  \quad~~\<open>warned: int,\<close> \\
-  \quad~~\<open>failed: int,\<close> \\
-  \quad~~\<open>finished: int,\<close> \\
-  \quad~~\<open>consolidated: bool}\<close> \\[2ex]
-
+  \begin{tabular}{ll}
   \<^bold>\<open>type\<close> \<open>node_result =\<close> \\
   \quad\<open>{node_name: string,\<close> \\
   \quad~~\<open>theory: string,\<close> \\
@@ -912,13 +924,17 @@
   \end{tabular}
 
   \<^medskip>
+  The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
+  current version of theory files to it, while dependencies are resolved
+  implicitly. The command succeeds eventually, when all theories have been
+  \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
+  (\secref{sec:json-types}): the outermost command structure has finished (or
+  failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
 
-  The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
-  current version of given theory files to it: theory dependencies are
-  resolved implicitly. The command succeeds eventually, when all theories have
-  been \<^emph>\<open>consolidated\<close> in the sense that the outermost command structure has
-  finished (or failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been
-  checked.
+  Already used theories persist in the session until purged explicitly. This
+  also means that repeated invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it
+  could make sense to do that with different values for \<open>pretty_margin\<close> or
+  \<open>unicode_symbols\<close> to get different formatting for \<open>errors\<close> or \<open>messages\<close>.
 \<close>
 
 
@@ -929,63 +945,62 @@
   was created (possibly on a different client connection).
 
   \<^medskip>
-  The \<open>theories\<close> field specifies theory names as in \<^theory_text>\<open>theory imports\<close> or in
-  session ROOT \<^verbatim>\<open>theories\<close>: an explicit source position for these theory name
-  specifications may be given as well, which is occasionally useful for
-  precise error locations.
+  The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
+  ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
+  specifications may be given, which is occasionally useful for precise error
+  locations.
 
   \<^medskip>
   The \<open>qualifier\<close> field provides an alternative session qualifier for theories
   that are not formally recognized as a member of a particular session. The
   default is \<^verbatim>\<open>Draft\<close> as in Isabelle/jEdit. There is rarely a need to change
   that, as theory nodes are already uniquely identified by their physical
-  file-system location.
+  file-system location. This already allows reuse of theory base names with
+  the same session qualifier --- as long as these theories are not used
+  together (e.g.\ in \<^theory_text>\<open>imports\<close>).
 
-  \<^medskip>
-  The \<open>master_dir\<close> field explicit specifies the formal master directory of the
-  imported theory. Normally this is determined implicitly from the parent
-  directory of the physical theory file location.
+  \<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
+  the imported theory. Normally this is determined implicitly from the parent
+  directory of the theory file.
 
   \<^medskip>
   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
-  default is for classic console output. Formatting happens at the end of
-  \<^verbatim>\<open>use_theories\<close>, when all prover messages produced are exported to the
-  client.
+  default is suitable for classic console output. Formatting happens at the
+  end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.
 
   \<^medskip>
-  The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> means that message output is
-  rendered for direct output on a Unicode capable channel, ideally with the
-  Isabelle fonts as in Isabelle/jEdit (or Isabelle HTML output). The default
-  is to keep the symbolic representation of Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead
-  of its rendering as \<open>\<forall>\<close>. This means the client needs to perform its own
-  rendering to present it to the end-user.
+  The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> renders message output for direct
+  output on a Unicode capable channel, ideally with the Isabelle fonts as in
+  Isabelle/jEdit. The default is to keep the symbolic representation of
+  Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead of its rendering as \<open>\<forall>\<close>. This means the
+  client needs to perform its own rendering before presenting it to the
+  end-user.
 \<close>
 
+
 subsubsection \<open>Results\<close>
 
 text \<open>
   The \<open>ok\<close> field indicates overall success of processing the specified
   theories with all their dependencies.
 
-  When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively,
-  including position information for the theory nodes where the error happened
-  (this includes imported theories).
+  When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively
+  (including imported theories). The messages contain position information for
+  the original theory nodes.
 
   \<^medskip>
-  The \<open>nodes\<close> field provides more detailed information about each imported
-  theory node. Here the individual fields are as follows:
+  The \<open>nodes\<close> field provides detailed information about each imported theory
+  node. The individual fields are as follows:
 
   \<^item> \<open>node_name\<close>: the physical name for the theory node, based on its
-  file-system location;\<^footnote>\<open>Clients may recognize the originally provided
-  file-names after careful normalization in the file-system of the server.\<close>
+  file-system location;
 
-  \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close> or
-  \<^verbatim>\<open>Draft.Test\<close>;
+  \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close>;
 
   \<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
   \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
 
-  \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory note
+  \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
   (\<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>, etc.).
 \<close>