src/Doc/System/Server.thy
changeset 67918 7dc204623770
parent 67917 d13b2dd20f5e
child 67919 dd90faed43b2
     1.1 --- a/src/Doc/System/Server.thy	Wed Mar 21 21:50:28 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Thu Mar 22 14:27:32 2018 +0100
     1.3 @@ -76,28 +76,29 @@
     1.4  
     1.5    \<^medskip>
     1.6    Option \<^verbatim>\<open>-c\<close> connects the console in/out channels after the initial check
     1.7 -  for a suitable server process. Note that the @{tool client} tool
     1.8 -  (\secref{sec:tool-client}) provides a more convenient way to do this
     1.9 -  interactively, together with command-line editor support.
    1.10 -
    1.11 -  \<^medskip>
    1.12 -  Option \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
    1.13 -  details.
    1.14 -
    1.15 -  \<^medskip>
    1.16 -  Option \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a \<^verbatim>\<open>shutdown\<close>
    1.17 -  command.
    1.18 +  for a suitable server process. Also note that the @{tool client} tool
    1.19 +  (\secref{sec:tool-client}) provides a command-line editor to interact with
    1.20 +  the server.
    1.21  
    1.22    \<^medskip>
    1.23    Option \<^verbatim>\<open>-L\<close> specifies a log file for exceptional output of internal server
    1.24    and session operations.
    1.25 +
    1.26 +  \<^medskip>
    1.27 +  Operation \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
    1.28 +  details.
    1.29 +
    1.30 +  \<^medskip>
    1.31 +  Operation \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a
    1.32 +  \<^verbatim>\<open>shutdown\<close> command.
    1.33  \<close>
    1.34  
    1.35  
    1.36  subsection \<open>Client \label{sec:tool-client}\<close>
    1.37  
    1.38  text \<open>
    1.39 -  The @{tool_def client} provides console interaction for Isabelle servers:
    1.40 +  The @{tool_def client} tool provides console interaction for Isabelle
    1.41 +  servers:
    1.42    @{verbatim [display]
    1.43  \<open>Usage: isabelle client [OPTIONS]
    1.44  
    1.45 @@ -107,8 +108,8 @@
    1.46  
    1.47    Console interaction for Isabelle server (with line-editor).\<close>}
    1.48  
    1.49 -  This is a convenient wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
    1.50 -  experimentation, wrapped into @{setting ISABELLE_LINE_EDITOR} if available.
    1.51 +  This is a wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
    1.52 +  experimentation, which uses @{setting ISABELLE_LINE_EDITOR} if available.
    1.53    The server name is sufficient for identification, as the client can
    1.54    determine the connection details from the local database of active servers.
    1.55  
    1.56 @@ -126,10 +127,9 @@
    1.57    Ensure that a particular server instance is running in the background:
    1.58    @{verbatim [display] \<open>isabelle server -n test &\<close>}
    1.59  
    1.60 -  Here the first line of output presents the connection details:\<^footnote>\<open>This
    1.61 -  information may be used in an independent TCP client, while the
    1.62 -  Isabelle/Scala tool merely needs the server name to access the database of
    1.63 -  servers.\<close>
    1.64 +  The first line of output presents the connection details:\<^footnote>\<open>This information
    1.65 +  may be used in other TCP clients, without access to Isabelle/Scala and the
    1.66 +  underlying database of running servers.\<close>
    1.67    @{verbatim [display] \<open>server "test" = 127.0.0.1:4711 (password "XYZ")\<close>}
    1.68  
    1.69    \<^medskip>
    1.70 @@ -152,7 +152,7 @@
    1.71    possible to reconnect again, and have multiple connections at the same time.
    1.72  
    1.73    \<^medskip>
    1.74 -  Finally, exit the named server on the command-line:
    1.75 +  Exit the named server on the command-line:
    1.76    @{verbatim [display] \<open>isabelle server -n test -x\<close>}
    1.77  \<close>
    1.78  
    1.79 @@ -161,12 +161,12 @@
    1.80  
    1.81  text \<open>
    1.82    The Isabelle server listens on a regular TCP socket, using a line-oriented
    1.83 -  protocol of structured messages: input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
    1.84 +  protocol of structured messages. Input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
    1.85    (via \<^verbatim>\<open>OK\<close> or \<^verbatim>\<open>ERROR\<close>) are strictly alternating on the toplevel, but
    1.86    commands may also return a \<^emph>\<open>task\<close> identifier to indicate an ongoing
    1.87    asynchronous process that is joined later (via \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>).
    1.88    Asynchronous \<^verbatim>\<open>NOTE\<close> messages may occur at any time: they are independent of
    1.89 -  the main command-reply protocol.
    1.90 +  the main command-result protocol.
    1.91  
    1.92    For example, the synchronous \<^verbatim>\<open>echo\<close> command immediately returns its
    1.93    argument as \<^verbatim>\<open>OK\<close> result. In contrast, the asynchronous \<^verbatim>\<open>session_build\<close>
    1.94 @@ -176,7 +176,7 @@
    1.95    may emit asynchronous messages of the form \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>
    1.96    to inform about its progress. Due to the explicit task identifier, the
    1.97    client can show these messages in the proper context, e.g.\ a GUI window for
    1.98 -  the session build job.
    1.99 +  this particular session build job.
   1.100  
   1.101    \medskip Subsequently, the protocol message formats are described in further
   1.102    detail.
   1.103 @@ -191,22 +191,22 @@
   1.104    particular length. Messages are written as a single chunk that is flushed
   1.105    immediately.
   1.106  
   1.107 -  The message boundary is determined as follows:
   1.108 +  Message boundaries are determined as follows:
   1.109  
   1.110      \<^item> A \<^emph>\<open>short message\<close> consists of a single line: it is a sequence of
   1.111      arbitrary bytes excluding CR (13) and LF (10), and terminated by CR-LF or
   1.112      just LF.
   1.113  
   1.114 -    \<^item> A \<^emph>\<open>long message\<close> starts with a single line as above, which consists
   1.115 -    only of decimal digits: that is interpreted as length of the subsequent
   1.116 -    block of arbitrary bytes. A final line-terminator may be included here,
   1.117 +    \<^item> A \<^emph>\<open>long message\<close> starts with a single that consists only of decimal
   1.118 +    digits: these are interpreted as length of the subsequent block of
   1.119 +    arbitrary bytes. A final line-terminator (as above) may be included here,
   1.120      but is not required.
   1.121  
   1.122    Messages in JSON format (see below) always fit on a single line, due to
   1.123    escaping of newline characters within string literals. This is convenient
   1.124    for interactive experimentation, but it can impact performance for very long
   1.125    messages. If the message byte-length is given on the preceding line, the
   1.126 -  server can read the message efficiently as a single block.
   1.127 +  server can read the message more efficiently as a single block.
   1.128  \<close>
   1.129  
   1.130  
   1.131 @@ -232,13 +232,13 @@
   1.132      \<^item> \<open>name argument\<close> such that:
   1.133  
   1.134      \<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
   1.135 -    ``\<^verbatim>\<open>_\<close>'' (underscore), or ``\<^verbatim>\<open>.\<close>'' (dot),
   1.136 +    ``\<^verbatim>\<open>_\<close>'', ``\<^verbatim>\<open>.\<close>'',
   1.137  
   1.138      \<^item> the separator between \<open>name\<close> and \<open>argument\<close> is the longest possible
   1.139      sequence of ASCII blanks (it could be empty, e.g.\ when the argument
   1.140      starts with a quote or bracket),
   1.141  
   1.142 -    \<^item> \<open>argument\<close> is the rest of the message without the line terminator.
   1.143 +    \<^item> \<open>argument\<close> is the rest of the message without line terminator.
   1.144  
   1.145    \<^medskip>
   1.146    Input messages are sent from the client to the server. Here the \<open>name\<close>
   1.147 @@ -283,7 +283,8 @@
   1.148    Whenever a new client opens the server socket, the initial message needs to
   1.149    be its unique password. The server replies either with \<^verbatim>\<open>OK\<close> (and some
   1.150    information about the Isabelle version) or by silent disconnection of what
   1.151 -  is considered an illegal connection attempt.
   1.152 +  is considered an illegal connection attempt. Note that @{tool client}
   1.153 +  already presents the correct password internally.
   1.154  
   1.155    Server passwords are created as Universally Unique Identifier (UUID) in
   1.156    Isabelle/Scala and stored in a per-user database, with restricted
   1.157 @@ -301,7 +302,7 @@
   1.158    Isabelle/Scala, with single argument and result (regular or error). Both the
   1.159    argument and the result may consist of type \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close>.
   1.160    An error result typically consists of a JSON object with error message and
   1.161 -  potentially further fields (this resembles exceptions in Scala).
   1.162 +  potentially further result fields (this resembles exceptions in Scala).
   1.163  
   1.164    These are the protocol exchanges for both cases of command execution:
   1.165    \begin{center}
   1.166 @@ -318,11 +319,11 @@
   1.167  
   1.168  text \<open>
   1.169    An \<^emph>\<open>asynchronous command\<close> corresponds to an ongoing process that finishes
   1.170 -  or fails eventually, while emitting arbitrary notifications intermediately.
   1.171 -  Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close> and
   1.172 -  the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad command
   1.173 -  syntax. For a running task, the termination is indicated later by
   1.174 -  \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result.
   1.175 +  or fails eventually, while emitting arbitrary notifications in between.
   1.176 +  Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close>
   1.177 +  giving the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad
   1.178 +  command syntax. For a running task, the termination is indicated later by
   1.179 +  \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result value.
   1.180  
   1.181    These are the protocol exchanges for various cases of command task
   1.182    execution:
   1.183 @@ -332,7 +333,6 @@
   1.184    \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   1.185    immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> \\
   1.186    intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   1.187 -  intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   1.188    (a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   1.189    (b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FAILED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\[3ex]
   1.190    \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   1.191 @@ -341,34 +341,18 @@
   1.192    \end{center}
   1.193  
   1.194    All asynchronous messages are decorated with the task identifier that was
   1.195 -  revealed in the immediate (synchronous) result. Thus it is possible to emit
   1.196 -  further asynchronous commands and dispatch the mingled stream of
   1.197 +  revealed in the immediate (synchronous) result. Thus the client can
   1.198 +  invoke further asynchronous commands and still dispatch the resulting stream of
   1.199    asynchronous messages properly.
   1.200  
   1.201    The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
   1.202    prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is not guaranteed:
   1.203 -  the cancel event may come too late or the task may just ignore it.
   1.204 +  the cancel event may come too late or the running process may just ignore
   1.205 +  it.
   1.206  \<close>
   1.207  
   1.208  
   1.209 -section \<open>Server commands and results\<close>
   1.210 -
   1.211 -text \<open>
   1.212 -  Here follows an overview of particular Isabelle server commands with their
   1.213 -  results, which are usually represented as JSON values. The general format of
   1.214 -  input and output messages is described in
   1.215 -  \secref{sec:input-output-messages}. The relevant Isabelle/Scala source files
   1.216 -  are:
   1.217 -
   1.218 -  \<^medskip>
   1.219 -  \begin{tabular}{l}
   1.220 -  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
   1.221 -  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close>
   1.222 -  \end{tabular}
   1.223 -\<close>
   1.224 -
   1.225 -
   1.226 -subsection \<open>Types for JSON values\<close>
   1.227 +section \<open>Types for JSON values \label{sec:json-types}\<close>
   1.228  
   1.229  text \<open>
   1.230    In order to specify concrete JSON types for command arguments and result
   1.231 @@ -381,24 +365,25 @@
   1.232        'bool' | 'int' | 'long' | 'double' | 'string' | '[' @{syntax type} ']' |
   1.233        '{' (@{syntax field_type} ',' *) '}' |
   1.234        @{syntax type} '\<oplus>' @{syntax type} |
   1.235 -      @{syntax type} '|' @{syntax type}
   1.236 +      @{syntax type} '|' @{syntax type} |
   1.237 +      '(' @{syntax type} ')'
   1.238      ;
   1.239      @{syntax field_type}: @{syntax name} ('?'?) ':' @{syntax type}
   1.240    \<close>
   1.241  
   1.242 -  This is a simplified version of interfaces in
   1.243 -  TypeScript.\<^footnote>\<open>\<^url>\<open>https://www.typescriptlang.org/docs/handbook/interfaces.html\<close>\<close>
   1.244 -  The meaning of these types is specified wrt. the implementation in
   1.245 -  Isabelle/Scala as follows.
   1.246 +  This is a simplified variation of TypeScript
   1.247 +  interfaces.\<^footnote>\<open>\<^url>\<open>https://www.typescriptlang.org/docs/handbook/interfaces.html\<close>\<close>
   1.248 +  The meaning of these types is specified wrt. the Isabelle/Scala
   1.249 +  implementation as follows.
   1.250  
   1.251    \<^item> A \<open>name\<close> refers to a type defined elsewhere. The environment of type
   1.252    definitions is given informally: put into proper foundational order, it
   1.253 -  needs to specify a strongly normalizing system; type definitions may not be
   1.254 -  recursive.
   1.255 +  needs to specify a strongly normalizing system of syntactic abbreviations;
   1.256 +  type definitions may not be recursive.
   1.257  
   1.258    \<^item> A \<open>value\<close> in JSON notation represents the singleton type of the given
   1.259 -  item. For example, the string \<^verbatim>\<open>"error"\<close> can be used is the type for a slot
   1.260 -  that is guaranteed to contain that constant.
   1.261 +  item. For example, the string \<^verbatim>\<open>"error"\<close> can be used as type for a slot that
   1.262 +  is guaranteed to contain that constant.
   1.263  
   1.264    \<^item> Type \<open>any\<close> is the super type of all other types: it is an untyped slot in
   1.265    the specification and corresponds to \<^verbatim>\<open>Any\<close> or \<^verbatim>\<open>JSON.T\<close> in Isabelle/Scala.
   1.266 @@ -408,7 +393,7 @@
   1.267    ``Null References: The Billion Dollar Mistake'' by Tony Hoare
   1.268    \<^url>\<open>https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare\<close>.\<close>
   1.269  
   1.270 -  \<^item> Type \<open>bool\<close> is the type of the truth values \<open>true\<close> and \<open>false\<close>; it
   1.271 +  \<^item> Type \<open>bool\<close> is the type of the truth values \<^verbatim>\<open>true\<close> and \<^verbatim>\<open>false\<close>; it
   1.272    corresponds to \<^verbatim>\<open>Boolean\<close> in Scala.
   1.273  
   1.274    \<^item> Types \<open>int\<close>, \<open>long\<close>, \<open>double\<close> are specific versions of the generic
   1.275 @@ -422,18 +407,18 @@
   1.276  
   1.277    \<^item> Type \<open>[t]\<close> is the array (or list) type over \<open>t\<close>; it corresponds to
   1.278    \<^verbatim>\<open>List[t]\<close> in Scala. The list type is co-variant as usual (i.e.\ monotonic
   1.279 -  wrt. the subtype order).
   1.280 +  wrt. the subtype relation).
   1.281  
   1.282    \<^item> Object types describe the possible content of JSON records, with field
   1.283    names and types. A question mark after a field name means that it is
   1.284 -  optional: in Scala this could refer to an explicit type \<^verbatim>\<open>Option[t]\<close>. For
   1.285 -  example, \<open>{a: int, b?: string}\<close> corresponds to a Scala case class with
   1.286 -  arguments \<^verbatim>\<open>a: Int\<close>, \<^verbatim>\<open>b: Option[String]\<close>.
   1.287 +  optional. In Scala this could refer to an explicit type \<^verbatim>\<open>Option[t]\<close>, e.g.\
   1.288 +  \<open>{a: int, b?: string}\<close> corresponding to a Scala case class with arguments
   1.289 +  \<^verbatim>\<open>a: Int\<close>, \<^verbatim>\<open>b: Option[String]\<close>.
   1.290  
   1.291    Alternatively, optional fields can have a default value. If nothing else is
   1.292 -  specified, the standard default value is the ``empty'' value of a type,
   1.293 -  i.e.\ \<^verbatim>\<open>0\<close> for the number types, \<^verbatim>\<open>false\<close> for \<open>bool\<close>, or the empty string,
   1.294 -  array, object etc.
   1.295 +  specified, a standard ``empty value'' is used for each type, i.e.\ \<^verbatim>\<open>0\<close> for
   1.296 +  the number types, \<^verbatim>\<open>false\<close> for \<open>bool\<close>, or the empty string, array, object
   1.297 +  etc.
   1.298  
   1.299    Object types are \<^emph>\<open>permissive\<close> in the sense that only the specified field
   1.300    names need to conform to the given types, but unspecified fields may be
   1.301 @@ -447,18 +432,20 @@
   1.302    \<^item> The type expression \<open>t\<^sub>1 | t\<^sub>2\<close> is the disjoint union of two types, either
   1.303    one of the two cases may occur.
   1.304  
   1.305 +  \<^item> Parentheses \<open>(t)\<close> merely group type expressions syntactically.
   1.306 +
   1.307  
   1.308    These types correspond to JSON values in an obvious manner, which is not
   1.309    further described here. For example, the JSON array \<^verbatim>\<open>[1, 2, 3]\<close> conforms to
   1.310    types \<open>[int]\<close>, \<open>[long]\<close>, \<open>[double]\<close>, \<open>[any]\<close>, \<open>any\<close>.
   1.311  
   1.312    Note that JSON objects require field names to be quoted, but the type
   1.313 -  language omits quotes for clarity. Thus \<^verbatim>\<open>{"a": 42, "b": "xyz"}\<close> conforms to
   1.314 -  the type \<open>{a: int, b: string}\<close>, for example.
   1.315 +  language omits quotes for clarity. Thus the object \<^verbatim>\<open>{"a": 42, "b": "xyz"}\<close>
   1.316 +  conforms to the type \<open>{a: int, b: string}\<close>, for example.
   1.317  
   1.318    \<^medskip>
   1.319 -  The absence of an argument or result is represented by type \<^verbatim>\<open>Unit\<close> in
   1.320 -  Isabelle/Scala: it is written as empty text in the message \<open>argument\<close>
   1.321 +  The absence of an argument or result is represented by the Scala type
   1.322 +  \<^verbatim>\<open>Unit\<close>: it is written as empty text in the message \<open>argument\<close>
   1.323    (\secref{sec:input-output-messages}). This is not part of the JSON language.
   1.324  
   1.325    Server replies have name tags like \<^verbatim>\<open>OK\<close>, \<^verbatim>\<open>ERROR\<close>: these are used literally
   1.326 @@ -467,16 +454,17 @@
   1.327    list (JSON array) of strings.
   1.328  
   1.329    \<^bigskip>
   1.330 -  Here are some common type definitions, for use in the subsequent
   1.331 -  specifications of command arguments and results.
   1.332 +  Here are some common type definitions, for use in particular specifications
   1.333 +  of command arguments and results.
   1.334  
   1.335    \<^item> \<^bold>\<open>type\<close>~\<open>position = {line?: int, offset?: int, end_offset?: int, file?:
   1.336 -  string, id?: long}\<close> describes a source position within Isabelle source text.
   1.337 -  Only the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
   1.338 +  string, id?: long}\<close> describes a source position within Isabelle text. Only
   1.339 +  the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
   1.340    Detailed \<open>offset\<close> and \<open>end_offset\<close> positions are counted according to
   1.341    Isabelle symbols, see @{ML_type Symbol.symbol} in Isabelle/ML @{cite
   1.342 -  "isabelle-implementation"}. The position \<open>id\<close> belongs to the internal
   1.343 -  representation of command transactions in the Isabelle/PIDE protocol.
   1.344 +  "isabelle-implementation"}. The position \<open>id\<close> belongs to the representation
   1.345 +  of command transactions in the Isabelle/PIDE protocol: it normally does not
   1.346 +  occur in externalized positions.
   1.347  
   1.348    \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
   1.349    the \<open>kind\<close> provides some hint about the role and importance of the message.
   1.350 @@ -492,9 +480,9 @@
   1.351    \<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
   1.352    string, session: string}\<close> reports formal progress in loading theories (e.g.\
   1.353    when building a session image). Apart from a regular output message, it also
   1.354 -  reveals the formal theory name (e.g.\ \<^verbatim>\<open>HOL.Nat\<close>) and session name (e.g.\
   1.355 -  \<^verbatim>\<open>HOL\<close>). Note that some rare theory names lack a proper session prefix, e.g.
   1.356 -  theory \<^verbatim>\<open>Main\<close> in session \<^verbatim>\<open>HOL\<close>.
   1.357 +  reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
   1.358 +  \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
   1.359 +  e.g. theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
   1.360  
   1.361    \<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
   1.362    common Isabelle timing information in seconds, usually with a precision of
   1.363 @@ -506,7 +494,7 @@
   1.364    identifiers are created as private random numbers of the server and only
   1.365    revealed to the client that creates a certain resource (e.g.\ task or
   1.366    session). A client may disclose this information for use in a different
   1.367 -  client connection: e.g.\ this allows to share sessions between multiple
   1.368 +  client connection: this allows to share sessions between multiple
   1.369    connections.
   1.370  
   1.371    Client commands need to provide syntactically wellformed UUIDs: this is
   1.372 @@ -515,8 +503,34 @@
   1.373  
   1.374    \<^item> \<^bold>\<open>type\<close>~\<open>task = {task: uuid}\<close> identifies a newly created asynchronous task
   1.375    and thus allows the client to control it by the \<^verbatim>\<open>cancel\<close> command. The same
   1.376 -  task identification is included in messages and the final result produced by
   1.377 -  this task.
   1.378 +  task identification is included in all messages produced by this task.
   1.379 +
   1.380 +  \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
   1.381 +  int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
   1.382 +  represents a formal theory node status of the PIDE document model. Fields
   1.383 +  \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close> account
   1.384 +  for individual commands within a theory node; \<open>ok\<close> is an abstraction for
   1.385 +  \<open>failed = 0\<close>. The \<open>consolidated\<close> flag indicates whether the outermost theory
   1.386 +  command structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has
   1.387 +  been checked.
   1.388 +\<close>
   1.389 +
   1.390 +
   1.391 +section \<open>Server commands and results\<close>
   1.392 +
   1.393 +text \<open>
   1.394 +  Here follows an overview of particular Isabelle server commands with their
   1.395 +  results, which are usually represented as JSON values with types according
   1.396 +  to \secref{sec:json-types}. The general format of input and output messages
   1.397 +  is described in \secref{sec:input-output-messages}. The relevant
   1.398 +  Isabelle/Scala source files are:
   1.399 +
   1.400 +  \<^medskip>
   1.401 +  \begin{tabular}{l}
   1.402 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
   1.403 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close> \\
   1.404 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/General/json.scala\<close> \\
   1.405 +  \end{tabular}
   1.406  \<close>
   1.407  
   1.408  
   1.409 @@ -528,9 +542,9 @@
   1.410    \end{tabular}
   1.411    \<^medskip>
   1.412  
   1.413 -  The \<^verbatim>\<open>help\<close> command has no argument and returns the list of command names
   1.414 -  known to the server. This is occasionally useful for interactive
   1.415 -  experimentation (see also @{tool client} in \secref{sec:tool-client}).
   1.416 +  The \<^verbatim>\<open>help\<close> command has no argument and returns the list of server command
   1.417 +  names. This is occasionally useful for interactive experimentation (see also
   1.418 +  @{tool client} in \secref{sec:tool-client}).
   1.419  \<close>
   1.420  
   1.421  
   1.422 @@ -547,8 +561,8 @@
   1.423    regular result. This is occasionally useful for testing and interactive
   1.424    experimentation (see also @{tool client} in \secref{sec:tool-client}).
   1.425  
   1.426 -  The type of \<^verbatim>\<open>echo\<close> is actually more general than given above: \<^verbatim>\<open>Unit\<close>,
   1.427 -  \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close> are supported uniformly. Note that \<^verbatim>\<open>XML.Elem\<close> might
   1.428 +  The Scala type of \<^verbatim>\<open>echo\<close> is actually more general than given above:
   1.429 +  \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close> work uniformly. Note that \<^verbatim>\<open>XML.Elem\<close> might
   1.430    be difficult to type on the console in its YXML syntax
   1.431    (\secref{sec:yxml-vs-xml}).
   1.432  \<close>
   1.433 @@ -568,9 +582,8 @@
   1.434    connections!
   1.435  
   1.436    \<^medskip>
   1.437 -  Likewise, the command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server
   1.438 -  connection and issues a \<^verbatim>\<open>shutdown\<close> command (see also
   1.439 -  \secref{sec:tool-server}).
   1.440 +  The command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server connection
   1.441 +  and issues a \<^verbatim>\<open>shutdown\<close> command (see also \secref{sec:tool-server}).
   1.442  \<close>
   1.443  
   1.444  
   1.445 @@ -583,17 +596,17 @@
   1.446    \end{tabular}
   1.447    \<^medskip>
   1.448  
   1.449 -  The command invocation \<^verbatim>\<open>cancel "\<close>\<open>id\<close>\<^verbatim>\<open>"\<close> attempts to cancel the specified
   1.450 -  task.
   1.451 +  The command invocation \<^verbatim>\<open>cancel "\<close>\<open>uuid\<close>\<^verbatim>\<open>"\<close> attempts to cancel the
   1.452 +  specified task.
   1.453  
   1.454    Cancellation is merely a hint that the client prefers an ongoing process to
   1.455    be stopped. The command always succeeds formally, but it may get ignored by
   1.456 -  a task that is still running, or it might refer to a non-existing or
   1.457 -  no-longer existing task without producing an error.
   1.458 +  a task that is still running; it might also refer to a non-existing or
   1.459 +  no-longer existing task (without producing an error).
   1.460  
   1.461    Successful cancellation typically leads to an asynchronous failure of type
   1.462 -  \<^verbatim>\<open>FAILED {\<close>\<open>task: string, message: \<close>\<^verbatim>\<open>"Interrupt"}\<close> --- or a slightly
   1.463 -  different message, depending how the task handles the event.
   1.464 +  \<^verbatim>\<open>FAILED {\<close>\<open>task: uuid, message:\<close>~\<^verbatim>\<open>"Interrupt"}\<close>. A different message is
   1.465 +  also possible, depending how the task handles the event.
   1.466  \<close>
   1.467  
   1.468  
   1.469 @@ -621,43 +634,45 @@
   1.470    \quad~~\<open>system_mode?: bool,\<close> \\
   1.471    \quad~~\<open>verbose?: bool}\<close> \\[2ex]
   1.472  
   1.473 -  \<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
   1.474 -  \quad\<open>{ok: bool,\<close> \\
   1.475 -  \quad~~\<open>return_code: int,\<close> \\
   1.476 -  \quad~~\<open>sessions: [session_build_result]}\<close> \\[2ex]
   1.477 -
   1.478    \<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
   1.479    \quad\<open>{session: string,\<close> \\
   1.480    \quad~~\<open>ok: bool,\<close> \\
   1.481    \quad~~\<open>return_code: int,\<close> \\
   1.482    \quad~~\<open>timeout: bool,\<close> \\
   1.483 -  \quad~~\<open>timing: timing}\<close> \\
   1.484 +  \quad~~\<open>timing: timing}\<close> \\[2ex]
   1.485 +
   1.486 +  \<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
   1.487 +  \quad\<open>{ok: bool,\<close> \\
   1.488 +  \quad~~\<open>return_code: int,\<close> \\
   1.489 +  \quad~~\<open>sessions: [session_build_result]}\<close> \\
   1.490    \end{tabular}
   1.491  \<close>
   1.492  
   1.493  text \<open>
   1.494 -  The \<^verbatim>\<open>session_build\<close> command prepares given a session image for interactive
   1.495 -  use of theories. This is a limited version of command-line tool @{tool
   1.496 -  build} (\secref{sec:tool-build}), with specific options to request a formal
   1.497 -  context of an interactive session: it also resembles options of @{tool
   1.498 -  jedit} @{cite "isabelle-jedit"}.
   1.499 +  The \<^verbatim>\<open>session_build\<close> command prepares a session image for interactive use of
   1.500 +  theories. This is a limited version of command-line tool @{tool build}
   1.501 +  (\secref{sec:tool-build}), with specific options to request a formal context
   1.502 +  for an interactive PIDE session.
   1.503  
   1.504    The build process is asynchronous, with notifications that inform about the
   1.505 -  progress of loaded theories. Some further human-readable messages may be
   1.506 -  output as well.
   1.507 +  progress of loaded theories. Some further informative messages are output as
   1.508 +  well.
   1.509  
   1.510    Coordination of independent build processes is at the discretion of the
   1.511 -  client: as for like @{tool build} there are no built-in measures against
   1.512 -  conflicting builds with overlapping hierarchies of session images.
   1.513 +  client (or end-user), just as for @{tool build} and @{tool jedit}. There is
   1.514 +  no built-in coordination of conflicting builds with overlapping hierarchies
   1.515 +  of session images. In the worst case, a session image produced by one task
   1.516 +  may get overwritten by another task!
   1.517  \<close>
   1.518  
   1.519  
   1.520  subsubsection \<open>Arguments\<close>
   1.521  
   1.522  text \<open>
   1.523 -  The field \<open>session\<close> is mandatory. It specifies the target session name:
   1.524 -  either directly (default) or indirectly (if \<open>required_session\<close> is
   1.525 -  \<^verbatim>\<open>true\<close>).
   1.526 +  The \<open>session\<close> field is mandatory. It specifies the target session name:
   1.527 +  either directly (default) or indirectly (if \<open>required_session\<close> is \<^verbatim>\<open>true\<close>).
   1.528 +  The build process will produce all required ancestor images for the
   1.529 +  specified target.
   1.530  
   1.531    \<^medskip>
   1.532    The environment of Isabelle system options is determined from \<open>preferences\<close>
   1.533 @@ -671,9 +686,9 @@
   1.534    operating-system contexts.
   1.535  
   1.536    \<^medskip>
   1.537 -  The \<open>dirs\<close> field specifies additional directories for session ROOT files
   1.538 -  (\secref{sec:session-root}). This augments the name space of available
   1.539 -  sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build} or @{tool jedit}.
   1.540 +  The \<open>dirs\<close> field specifies additional directories for session ROOT and ROOTS
   1.541 +  files (\secref{sec:session-root}). This augments the name space of available
   1.542 +  sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
   1.543  
   1.544    \<^medskip>
   1.545    The \<open>ancestor_session\<close> field specifies an alternative image as starting
   1.546 @@ -683,18 +698,18 @@
   1.547    session images of the hierarchy that are not used later on.
   1.548  
   1.549    \<^medskip>
   1.550 -  The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all existing sessions from
   1.551 -  reachable ROOT entries in the name space of theories with a proper
   1.552 -  session-qualified name (instead of referring to the file-system location).
   1.553 -  This could be relevant for the \<^verbatim>\<open>use_theories\<close> command
   1.554 +  The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all sessions from reachable
   1.555 +  ROOT entries into the name space of theories. This is relevant for proper
   1.556 +  session-qualified names, instead of referring to theory file names. The
   1.557 +  option enables the \<^verbatim>\<open>use_theories\<close> command
   1.558    (\secref{sec:command-use-theories}) to refer to arbitrary theories from
   1.559 -  other sessions. Note that considerable time is required to explore all
   1.560 -  accessible session directories and theory dependencies.
   1.561 +  other sessions, but considerable time is required to explore all accessible
   1.562 +  session directories and theory dependencies.
   1.563  
   1.564    \<^medskip>
   1.565 -  The \<open>focus_session\<close> field set to \<^verbatim>\<open>true\<close> to focuses on the target session:
   1.566 +  The \<open>focus_session\<close> field set to \<^verbatim>\<open>true\<close> focuses on the target session:
   1.567    the accessible name space of theories is restricted to sessions that are
   1.568 -  connected to it.
   1.569 +  connected to it in the imports graph.
   1.570  
   1.571    \<^medskip>
   1.572    The \<open>required_session\<close> field set to \<^verbatim>\<open>true\<close> indicates that the target image
   1.573 @@ -703,14 +718,13 @@
   1.574    the \<open>session\<close> itself can be loaded.
   1.575  
   1.576    \<^medskip>
   1.577 -  The \<open>system_mode\<close> field may be set to \<^verbatim>\<open>true\<close> to store session images and
   1.578 +  The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
   1.579    log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
   1.580    @{setting ISABELLE_OUTPUT} (which is normally in @{setting
   1.581 -  ISABELLE_HOME_USER}, i.e.\ the user's home directory). See also option \<^verbatim>\<open>-s\<close>
   1.582 -  in @{tool build} and @{tool jedit}.
   1.583 +  ISABELLE_HOME_USER}). See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
   1.584  
   1.585    \<^medskip>
   1.586 -  The \<open>verbose\<close> field may be set to \<^verbatim>\<open>true\<close> for extra verbosity. The effect is
   1.587 +  The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
   1.588    similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
   1.589  \<close>
   1.590  
   1.591 @@ -723,28 +737,29 @@
   1.592    Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
   1.593  
   1.594    For the client it is usually sufficient to print the messages in plain text,
   1.595 -  but note that \<open>theory_progress\<close> also reveals the internal \<open>theory\<close> and
   1.596 -  \<open>session\<close> names.
   1.597 +  but note that \<open>theory_progress\<close> also reveals formal \<open>theory\<close> and
   1.598 +  \<open>session\<close> names directly.
   1.599  \<close>
   1.600  
   1.601  
   1.602  subsubsection \<open>Results\<close>
   1.603  
   1.604  text \<open>
   1.605 -  The overall \<open>session_build_results\<close> contain both a summary and and entry
   1.606 -  \<open>session_build_result\<close> for each session in the build hierarchy, leading up
   1.607 -  to the specified target session. The result is always provided,
   1.608 -  independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or failure (\<^verbatim>\<open>FAILED\<close>
   1.609 -  task).
   1.610 +  The overall \<open>session_build_results\<close> contain both a summary and an entry
   1.611 +  \<open>session_build_result\<close> for each session in the build hierarchy. The result
   1.612 +  is always provided, independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or
   1.613 +  failure (\<^verbatim>\<open>FAILED\<close> task).
   1.614  
   1.615    The \<open>ok\<close> field tells abstractly, whether all required session builds came
   1.616 -  out as \<open>ok\<close>, i.e.\ \<open>return_code\<close>. A non-zero \<open>return_code\<close> indicates an
   1.617 -  error according to usual POSIX conventions for process exit.
   1.618 +  out as \<open>ok\<close>, i.e.\ with zero \<open>return_code\<close>. A non-zero \<open>return_code\<close>
   1.619 +  indicates an error according to usual POSIX conventions for process exit.
   1.620 +
   1.621 +  The individual \<open>session_build_result\<close> entries provide extra fields:
   1.622  
   1.623 -  For individual \<open>session_build_result\<close> entries, there are additional fields:
   1.624 -  \<open>timeout\<close> to tell if the build process was aborted after running too long,
   1.625 -  and \<open>timing\<close> for the overall process timing in the usual Isabelle format
   1.626 -  with elapsed, CPU, gc time.
   1.627 +  \<^item> \<open>timeout\<close> tells if the build process was aborted after running too long,
   1.628 +
   1.629 +  \<^item> \<open>timing\<close> gives the overall process timing in the usual Isabelle format
   1.630 +  with elapsed, CPU, GC time.
   1.631  \<close>
   1.632  
   1.633  
   1.634 @@ -780,25 +795,25 @@
   1.635    \<^medskip>
   1.636    The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with
   1.637    underlying Isabelle/ML process, based on a session image that it produces on
   1.638 -  demand in the same manner as \<^verbatim>\<open>session_build\<close>. Thus it accepts all
   1.639 -  \<open>session_build_args\<close> and produces similar notifications, but the detailed
   1.640 -  \<open>session_build_results\<close> are omitted.
   1.641 +  demand using \<^verbatim>\<open>session_build\<close>. Thus it accepts all \<open>session_build_args\<close> and
   1.642 +  produces similar notifications, but the detailed \<open>session_build_results\<close> are
   1.643 +  omitted.
   1.644  
   1.645    The session build and startup process is asynchronous: when the task is
   1.646 -  finished, the session remains active for commands such as \<^verbatim>\<open>use_theories\<close>
   1.647 -  (\secref{sec:command-use-theories}), until a \<^verbatim>\<open>session_stop\<close> or \<^verbatim>\<open>shutdown\<close>
   1.648 -  command is sent to the server.
   1.649 +  finished, the session remains active for commands, until a \<^verbatim>\<open>session_stop\<close>
   1.650 +  or \<^verbatim>\<open>shutdown\<close> command is sent to the server.
   1.651  
   1.652    Sessions are independent of client connections: it is possible to start a
   1.653    session and later apply \<^verbatim>\<open>use_theories\<close> on different connections, as long as
   1.654 -  the internal session identifier is known.
   1.655 +  the internal session identifier is known: shared theory imports will be used
   1.656 +  only once (and persist until purged explicitly).
   1.657  \<close>
   1.658  
   1.659  
   1.660  subsubsection \<open>Arguments\<close>
   1.661  
   1.662  text \<open>
   1.663 -  Most of the arguments are the same as for \<^verbatim>\<open>session_build\<close>
   1.664 +  Most arguments are shared with \<^verbatim>\<open>session_build\<close>
   1.665    (\secref{sec:command-session-build}).
   1.666  
   1.667    \<^medskip>
   1.668 @@ -826,6 +841,9 @@
   1.669  text \<open>
   1.670    Start a default Isabelle/HOL session:
   1.671    @{verbatim [display] \<open>session_start {"session": "HOL"}\<close>}
   1.672 +
   1.673 +  Start a session from the Archive of Formal Proofs:
   1.674 +  @{verbatim [display] \<open>session_start {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
   1.675  \<close>
   1.676  
   1.677  
   1.678 @@ -844,9 +862,9 @@
   1.679    \end{tabular}
   1.680  
   1.681    \<^medskip>
   1.682 -  The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified
   1.683 -  Isabelle/PIDE session. This asynchronous tasks usually finishes quickly.
   1.684 -  Failure only happens unusual situations, according to the return code of the
   1.685 +  The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified PIDE
   1.686 +  session. This asynchronous tasks usually finishes quickly. Failure only
   1.687 +  happens in unusual situations, according to the return code of the
   1.688    underlying Isabelle/ML process.
   1.689  \<close>
   1.690  
   1.691 @@ -854,17 +872,19 @@
   1.692  subsubsection \<open>Arguments\<close>
   1.693  
   1.694  text \<open>
   1.695 -  The \<open>session_id\<close> field is the UUID originally created by the server for the
   1.696 -  intended session.
   1.697 +  The \<open>session_id\<close> field provides the UUID originally created by the server
   1.698 +  for this session.
   1.699  \<close>
   1.700  
   1.701  
   1.702  subsubsection \<open>Results\<close>
   1.703  
   1.704  text \<open>
   1.705 -  The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process terminated
   1.706 -  properly. The \<open>return_code\<close> expresses this information according to usual
   1.707 -  POSIX conventions for process exit.
   1.708 +  The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process has
   1.709 +  terminated properly.
   1.710 +
   1.711 +  The \<open>return_code\<close> field expresses this information according to usual POSIX
   1.712 +  conventions for process exit.
   1.713  \<close>
   1.714  
   1.715  
   1.716 @@ -888,17 +908,9 @@
   1.717    \quad~~\<open>master_dir?: string,\<close> \\
   1.718    \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   1.719    \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
   1.720 +  \end{tabular}
   1.721  
   1.722 -  \<^bold>\<open>type\<close> \<open>node_status =\<close> \\
   1.723 -  \quad\<open>{ok: bool,\<close> \\
   1.724 -  \quad~~\<open>total: int,\<close> \\
   1.725 -  \quad~~\<open>unprocessed: int,\<close> \\
   1.726 -  \quad~~\<open>running: int,\<close> \\
   1.727 -  \quad~~\<open>warned: int,\<close> \\
   1.728 -  \quad~~\<open>failed: int,\<close> \\
   1.729 -  \quad~~\<open>finished: int,\<close> \\
   1.730 -  \quad~~\<open>consolidated: bool}\<close> \\[2ex]
   1.731 -
   1.732 +  \begin{tabular}{ll}
   1.733    \<^bold>\<open>type\<close> \<open>node_result =\<close> \\
   1.734    \quad\<open>{node_name: string,\<close> \\
   1.735    \quad~~\<open>theory: string,\<close> \\
   1.736 @@ -912,13 +924,17 @@
   1.737    \end{tabular}
   1.738  
   1.739    \<^medskip>
   1.740 +  The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
   1.741 +  current version of theory files to it, while dependencies are resolved
   1.742 +  implicitly. The command succeeds eventually, when all theories have been
   1.743 +  \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
   1.744 +  (\secref{sec:json-types}): the outermost command structure has finished (or
   1.745 +  failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
   1.746  
   1.747 -  The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
   1.748 -  current version of given theory files to it: theory dependencies are
   1.749 -  resolved implicitly. The command succeeds eventually, when all theories have
   1.750 -  been \<^emph>\<open>consolidated\<close> in the sense that the outermost command structure has
   1.751 -  finished (or failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been
   1.752 -  checked.
   1.753 +  Already used theories persist in the session until purged explicitly. This
   1.754 +  also means that repeated invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it
   1.755 +  could make sense to do that with different values for \<open>pretty_margin\<close> or
   1.756 +  \<open>unicode_symbols\<close> to get different formatting for \<open>errors\<close> or \<open>messages\<close>.
   1.757  \<close>
   1.758  
   1.759  
   1.760 @@ -929,63 +945,62 @@
   1.761    was created (possibly on a different client connection).
   1.762  
   1.763    \<^medskip>
   1.764 -  The \<open>theories\<close> field specifies theory names as in \<^theory_text>\<open>theory imports\<close> or in
   1.765 -  session ROOT \<^verbatim>\<open>theories\<close>: an explicit source position for these theory name
   1.766 -  specifications may be given as well, which is occasionally useful for
   1.767 -  precise error locations.
   1.768 +  The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
   1.769 +  ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
   1.770 +  specifications may be given, which is occasionally useful for precise error
   1.771 +  locations.
   1.772  
   1.773    \<^medskip>
   1.774    The \<open>qualifier\<close> field provides an alternative session qualifier for theories
   1.775    that are not formally recognized as a member of a particular session. The
   1.776    default is \<^verbatim>\<open>Draft\<close> as in Isabelle/jEdit. There is rarely a need to change
   1.777    that, as theory nodes are already uniquely identified by their physical
   1.778 -  file-system location.
   1.779 +  file-system location. This already allows reuse of theory base names with
   1.780 +  the same session qualifier --- as long as these theories are not used
   1.781 +  together (e.g.\ in \<^theory_text>\<open>imports\<close>).
   1.782  
   1.783 -  \<^medskip>
   1.784 -  The \<open>master_dir\<close> field explicit specifies the formal master directory of the
   1.785 -  imported theory. Normally this is determined implicitly from the parent
   1.786 -  directory of the physical theory file location.
   1.787 +  \<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
   1.788 +  the imported theory. Normally this is determined implicitly from the parent
   1.789 +  directory of the theory file.
   1.790  
   1.791    \<^medskip>
   1.792    The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
   1.793 -  default is for classic console output. Formatting happens at the end of
   1.794 -  \<^verbatim>\<open>use_theories\<close>, when all prover messages produced are exported to the
   1.795 -  client.
   1.796 +  default is suitable for classic console output. Formatting happens at the
   1.797 +  end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.
   1.798  
   1.799    \<^medskip>
   1.800 -  The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> means that message output is
   1.801 -  rendered for direct output on a Unicode capable channel, ideally with the
   1.802 -  Isabelle fonts as in Isabelle/jEdit (or Isabelle HTML output). The default
   1.803 -  is to keep the symbolic representation of Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead
   1.804 -  of its rendering as \<open>\<forall>\<close>. This means the client needs to perform its own
   1.805 -  rendering to present it to the end-user.
   1.806 +  The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> renders message output for direct
   1.807 +  output on a Unicode capable channel, ideally with the Isabelle fonts as in
   1.808 +  Isabelle/jEdit. The default is to keep the symbolic representation of
   1.809 +  Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead of its rendering as \<open>\<forall>\<close>. This means the
   1.810 +  client needs to perform its own rendering before presenting it to the
   1.811 +  end-user.
   1.812  \<close>
   1.813  
   1.814 +
   1.815  subsubsection \<open>Results\<close>
   1.816  
   1.817  text \<open>
   1.818    The \<open>ok\<close> field indicates overall success of processing the specified
   1.819    theories with all their dependencies.
   1.820  
   1.821 -  When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively,
   1.822 -  including position information for the theory nodes where the error happened
   1.823 -  (this includes imported theories).
   1.824 +  When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively
   1.825 +  (including imported theories). The messages contain position information for
   1.826 +  the original theory nodes.
   1.827  
   1.828    \<^medskip>
   1.829 -  The \<open>nodes\<close> field provides more detailed information about each imported
   1.830 -  theory node. Here the individual fields are as follows:
   1.831 +  The \<open>nodes\<close> field provides detailed information about each imported theory
   1.832 +  node. The individual fields are as follows:
   1.833  
   1.834    \<^item> \<open>node_name\<close>: the physical name for the theory node, based on its
   1.835 -  file-system location;\<^footnote>\<open>Clients may recognize the originally provided
   1.836 -  file-names after careful normalization in the file-system of the server.\<close>
   1.837 +  file-system location;
   1.838  
   1.839 -  \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close> or
   1.840 -  \<^verbatim>\<open>Draft.Test\<close>;
   1.841 +  \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close>;
   1.842  
   1.843    \<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
   1.844    \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
   1.845  
   1.846 -  \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory note
   1.847 +  \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
   1.848    (\<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>, etc.).
   1.849  \<close>
   1.850