merged
authorwenzelm
Thu Mar 22 17:06:15 2018 +0100 (14 months ago)
changeset 67926e6b9703b9656
parent 67910 b42473502373
parent 67925 74dce5658d4c
child 67927 0b70405b3969
merged
     1.1 --- a/src/Doc/System/Server.thy	Thu Mar 22 13:53:15 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Thu Mar 22 17:06:15 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 @@ -224,7 +224,7 @@
   1.132  \<close>
   1.133  
   1.134  
   1.135 -subsection \<open>Input and output messages\<close>
   1.136 +subsection \<open>Input and output messages \label{sec:input-output-messages}\<close>
   1.137  
   1.138  text \<open>
   1.139    Server input and output messages have a uniform format as follows:
   1.140 @@ -232,13 +232,13 @@
   1.141      \<^item> \<open>name argument\<close> such that:
   1.142  
   1.143      \<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
   1.144 -    ``\<^verbatim>\<open>_\<close>'' (underscore), or ``\<^verbatim>\<open>.\<close>'' (dot),
   1.145 +    ``\<^verbatim>\<open>_\<close>'', ``\<^verbatim>\<open>.\<close>'',
   1.146  
   1.147      \<^item> the separator between \<open>name\<close> and \<open>argument\<close> is the longest possible
   1.148      sequence of ASCII blanks (it could be empty, e.g.\ when the argument
   1.149      starts with a quote or bracket),
   1.150  
   1.151 -    \<^item> \<open>argument\<close> is the rest of the message without the line terminator.
   1.152 +    \<^item> \<open>argument\<close> is the rest of the message without line terminator.
   1.153  
   1.154    \<^medskip>
   1.155    Input messages are sent from the client to the server. Here the \<open>name\<close>
   1.156 @@ -283,7 +283,8 @@
   1.157    Whenever a new client opens the server socket, the initial message needs to
   1.158    be its unique password. The server replies either with \<^verbatim>\<open>OK\<close> (and some
   1.159    information about the Isabelle version) or by silent disconnection of what
   1.160 -  is considered an illegal connection attempt.
   1.161 +  is considered an illegal connection attempt. Note that @{tool client}
   1.162 +  already presents the correct password internally.
   1.163  
   1.164    Server passwords are created as Universally Unique Identifier (UUID) in
   1.165    Isabelle/Scala and stored in a per-user database, with restricted
   1.166 @@ -301,7 +302,7 @@
   1.167    Isabelle/Scala, with single argument and result (regular or error). Both the
   1.168    argument and the result may consist of type \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close>.
   1.169    An error result typically consists of a JSON object with error message and
   1.170 -  potentially further fields (this resembles exceptions in Scala).
   1.171 +  potentially further result fields (this resembles exceptions in Scala).
   1.172  
   1.173    These are the protocol exchanges for both cases of command execution:
   1.174    \begin{center}
   1.175 @@ -318,11 +319,11 @@
   1.176  
   1.177  text \<open>
   1.178    An \<^emph>\<open>asynchronous command\<close> corresponds to an ongoing process that finishes
   1.179 -  or fails eventually, while emitting arbitrary notifications intermediately.
   1.180 -  Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close> and
   1.181 -  the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad command
   1.182 -  syntax. For a running task, the termination is indicated later by
   1.183 -  \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result.
   1.184 +  or fails eventually, while emitting arbitrary notifications in between.
   1.185 +  Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close>
   1.186 +  giving the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad
   1.187 +  command syntax. For a running task, the termination is indicated later by
   1.188 +  \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result value.
   1.189  
   1.190    These are the protocol exchanges for various cases of command task
   1.191    execution:
   1.192 @@ -332,7 +333,6 @@
   1.193    \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   1.194    immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> \\
   1.195    intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   1.196 -  intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   1.197    (a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   1.198    (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.199    \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   1.200 @@ -341,14 +341,673 @@
   1.201    \end{center}
   1.202  
   1.203    All asynchronous messages are decorated with the task identifier that was
   1.204 -  revealed in the immediate (synchronous) result. Thus it is possible to emit
   1.205 -  further asynchronous commands and dispatch the mingled stream of
   1.206 +  revealed in the immediate (synchronous) result. Thus the client can
   1.207 +  invoke further asynchronous commands and still dispatch the resulting stream of
   1.208    asynchronous messages properly.
   1.209  
   1.210 -  The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
   1.211 -  prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result with error message
   1.212 -  \<^verbatim>\<open>Interrupt\<close>, but this is not guaranteed: the cancel event may come too
   1.213 -  late or the task may just ignore it.
   1.214 +  The synchronous command \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> tells the specified task
   1.215 +  to terminate prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is
   1.216 +  not guaranteed: the cancel event may come too late or the running process
   1.217 +  may just ignore it.
   1.218 +\<close>
   1.219 +
   1.220 +
   1.221 +section \<open>Types for JSON values \label{sec:json-types}\<close>
   1.222 +
   1.223 +text \<open>
   1.224 +  In order to specify concrete JSON types for command arguments and result
   1.225 +  messages, the following type definition language shall be used:
   1.226 +
   1.227 +  \<^rail>\<open>
   1.228 +    @{syntax type_def}: @'type' @{syntax name} '=' @{syntax type}
   1.229 +    ;
   1.230 +    @{syntax type}: @{syntax name} | @{syntax value} | 'any' | 'null' |
   1.231 +      'bool' | 'int' | 'long' | 'double' | 'string' | '[' @{syntax type} ']' |
   1.232 +      '{' (@{syntax field_type} ',' *) '}' |
   1.233 +      @{syntax type} '\<oplus>' @{syntax type} |
   1.234 +      @{syntax type} '|' @{syntax type} |
   1.235 +      '(' @{syntax type} ')'
   1.236 +    ;
   1.237 +    @{syntax field_type}: @{syntax name} ('?'?) ':' @{syntax type}
   1.238 +  \<close>
   1.239 +
   1.240 +  This is a simplified variation of TypeScript
   1.241 +  interfaces.\<^footnote>\<open>\<^url>\<open>https://www.typescriptlang.org/docs/handbook/interfaces.html\<close>\<close>
   1.242 +  The meaning of these types is specified wrt. the Isabelle/Scala
   1.243 +  implementation as follows.
   1.244 +
   1.245 +  \<^item> A \<open>name\<close> refers to a type defined elsewhere. The environment of type
   1.246 +  definitions is given informally: put into proper foundational order, it
   1.247 +  needs to specify a strongly normalizing system of syntactic abbreviations;
   1.248 +  type definitions may not be recursive.
   1.249 +
   1.250 +  \<^item> A \<open>value\<close> in JSON notation represents the singleton type of the given
   1.251 +  item. For example, the string \<^verbatim>\<open>"error"\<close> can be used as type for a slot that
   1.252 +  is guaranteed to contain that constant.
   1.253 +
   1.254 +  \<^item> Type \<open>any\<close> is the super type of all other types: it is an untyped slot in
   1.255 +  the specification and corresponds to \<^verbatim>\<open>Any\<close> or \<^verbatim>\<open>JSON.T\<close> in Isabelle/Scala.
   1.256 +
   1.257 +  \<^item> Type \<open>null\<close> is the type of the improper value \<open>null\<close>; it corresponds to
   1.258 +  type \<^verbatim>\<open>Null\<close> in Scala and is normally not used in Isabelle/Scala.\<^footnote>\<open>See also
   1.259 +  ``Null References: The Billion Dollar Mistake'' by Tony Hoare
   1.260 +  \<^url>\<open>https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare\<close>.\<close>
   1.261 +
   1.262 +  \<^item> Type \<open>bool\<close> is the type of the truth values \<^verbatim>\<open>true\<close> and \<^verbatim>\<open>false\<close>; it
   1.263 +  corresponds to \<^verbatim>\<open>Boolean\<close> in Scala.
   1.264 +
   1.265 +  \<^item> Types \<open>int\<close>, \<open>long\<close>, \<open>double\<close> are specific versions of the generic
   1.266 +  \<open>number\<close> type, corresponding to \<^verbatim>\<open>Int\<close>, \<^verbatim>\<open>Long\<close>, \<^verbatim>\<open>Double\<close> in Scala, but
   1.267 +  \<^verbatim>\<open>Long\<close> is limited to 53 bit precision.\<^footnote>\<open>Implementations of JSON typically
   1.268 +  standardize \<open>number\<close> to \<^verbatim>\<open>Double\<close>, which can absorb \<^verbatim>\<open>Int\<close> faithfully, but
   1.269 +  not all of \<^verbatim>\<open>Long\<close>.\<close>
   1.270 +
   1.271 +  \<^item> Type \<open>string\<close> represents Unicode text; it corresponds to type \<^verbatim>\<open>String\<close> in
   1.272 +  Scala.
   1.273 +
   1.274 +  \<^item> Type \<open>[t]\<close> is the array (or list) type over \<open>t\<close>; it corresponds to
   1.275 +  \<^verbatim>\<open>List[t]\<close> in Scala. The list type is co-variant as usual (i.e.\ monotonic
   1.276 +  wrt. the subtype relation).
   1.277 +
   1.278 +  \<^item> Object types describe the possible content of JSON records, with field
   1.279 +  names and types. A question mark after a field name means that it is
   1.280 +  optional. In Scala this could refer to an explicit type \<^verbatim>\<open>Option[t]\<close>, e.g.\
   1.281 +  \<open>{a: int, b?: string}\<close> corresponding to a Scala case class with arguments
   1.282 +  \<^verbatim>\<open>a: Int\<close>, \<^verbatim>\<open>b: Option[String]\<close>.
   1.283 +
   1.284 +  Alternatively, optional fields can have a default value. If nothing else is
   1.285 +  specified, a standard ``empty value'' is used for each type, i.e.\ \<^verbatim>\<open>0\<close> for
   1.286 +  the number types, \<^verbatim>\<open>false\<close> for \<open>bool\<close>, or the empty string, array, object
   1.287 +  etc.
   1.288 +
   1.289 +  Object types are \<^emph>\<open>permissive\<close> in the sense that only the specified field
   1.290 +  names need to conform to the given types, but unspecified fields may be
   1.291 +  present as well.
   1.292 +
   1.293 +  \<^item> The type expression \<open>t\<^sub>1 \<oplus> t\<^sub>2\<close> only works for two object types with
   1.294 +  disjoint field names: it is the concatenation of the respective @{syntax
   1.295 +  field_type} specifications taken together. For example: \<open>{task: string} \<oplus>
   1.296 +  {ok: bool}\<close> is the equivalent to \<open>{task: string, ok: bool}\<close>.
   1.297 +
   1.298 +  \<^item> The type expression \<open>t\<^sub>1 | t\<^sub>2\<close> is the disjoint union of two types, either
   1.299 +  one of the two cases may occur.
   1.300 +
   1.301 +  \<^item> Parentheses \<open>(t)\<close> merely group type expressions syntactically.
   1.302 +
   1.303 +
   1.304 +  These types correspond to JSON values in an obvious manner, which is not
   1.305 +  further described here. For example, the JSON array \<^verbatim>\<open>[1, 2, 3]\<close> conforms to
   1.306 +  types \<open>[int]\<close>, \<open>[long]\<close>, \<open>[double]\<close>, \<open>[any]\<close>, \<open>any\<close>.
   1.307 +
   1.308 +  Note that JSON objects require field names to be quoted, but the type
   1.309 +  language omits quotes for clarity. Thus the object \<^verbatim>\<open>{"a": 42, "b": "xyz"}\<close>
   1.310 +  conforms to the type \<open>{a: int, b: string}\<close>, for example.
   1.311 +
   1.312 +  \<^medskip>
   1.313 +  The absence of an argument or result is represented by the Scala type
   1.314 +  \<^verbatim>\<open>Unit\<close>: it is written as empty text in the message \<open>argument\<close>
   1.315 +  (\secref{sec:input-output-messages}). This is not part of the JSON language.
   1.316 +
   1.317 +  Server replies have name tags like \<^verbatim>\<open>OK\<close>, \<^verbatim>\<open>ERROR\<close>: these are used literally
   1.318 +  together with type specifications to indicate the particular name with the
   1.319 +  type of its argument, e.g.\ \<^verbatim>\<open>OK\<close>~\<open>[string]\<close> for a regular result that is a
   1.320 +  list (JSON array) of strings.
   1.321 +
   1.322 +  \<^bigskip>
   1.323 +  Here are some common type definitions, for use in particular specifications
   1.324 +  of command arguments and results.
   1.325 +
   1.326 +  \<^item> \<^bold>\<open>type\<close>~\<open>position = {line?: int, offset?: int, end_offset?: int, file?:
   1.327 +  string, id?: long}\<close> describes a source position within Isabelle text. Only
   1.328 +  the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
   1.329 +  Detailed \<open>offset\<close> and \<open>end_offset\<close> positions are counted according to
   1.330 +  Isabelle symbols, see @{ML_type Symbol.symbol} in Isabelle/ML @{cite
   1.331 +  "isabelle-implementation"}. The position \<open>id\<close> belongs to the representation
   1.332 +  of command transactions in the Isabelle/PIDE protocol: it normally does not
   1.333 +  occur in externalized positions.
   1.334 +
   1.335 +  \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
   1.336 +  the \<open>kind\<close> provides some hint about the role and importance of the message.
   1.337 +  The main message kinds are \<^verbatim>\<open>writeln\<close> (for regular output), \<^verbatim>\<open>warning\<close>,
   1.338 +  \<^verbatim>\<open>error\<close>. Messages without explicit kind can be treated like \<^verbatim>\<open>writeln\<close>.
   1.339 +
   1.340 +  \<^item> \<^bold>\<open>type\<close>~\<open>error_message = {kind:\<close>~\<^verbatim>\<open>"error"\<close>\<open>, message: string}\<close> refers to
   1.341 +  error messages in particular. These occur routinely with \<^verbatim>\<open>ERROR\<close> or
   1.342 +  \<^verbatim>\<open>FAILED\<close> replies, but also as initial command syntax errors (which are
   1.343 +  omitted in the command specifications below).
   1.344 +
   1.345 +  \<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
   1.346 +  string, session: string}\<close> reports formal progress in loading theories (e.g.\
   1.347 +  when building a session image). Apart from a regular output message, it also
   1.348 +  reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
   1.349 +  \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
   1.350 +  e.g. theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
   1.351 +
   1.352 +  \<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
   1.353 +  common Isabelle timing information in seconds, usually with a precision of
   1.354 +  three digits after the point (whole milliseconds).
   1.355 +
   1.356 +  \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
   1.357 +  as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
   1.358 +  \<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/UUID.html\<close>.\<close> Such
   1.359 +  identifiers are created as private random numbers of the server and only
   1.360 +  revealed to the client that creates a certain resource (e.g.\ task or
   1.361 +  session). A client may disclose this information for use in a different
   1.362 +  client connection: this allows to share sessions between multiple
   1.363 +  connections.
   1.364 +
   1.365 +  Client commands need to provide syntactically wellformed UUIDs: this is
   1.366 +  trivial to achieve by using only identifiers that have been produced by the
   1.367 +  server beforehand.
   1.368 +
   1.369 +  \<^item> \<^bold>\<open>type\<close>~\<open>task = {task: uuid}\<close> identifies a newly created asynchronous task
   1.370 +  and thus allows the client to control it by the \<^verbatim>\<open>cancel\<close> command. The same
   1.371 +  task identification is included in all messages produced by this task.
   1.372 +
   1.373 +  \<^item> \<^bold>\<open>type\<close> \<open>session_id = {session_id: uuid}\<close> identifies a newly created PIDE
   1.374 +  session managed by the server. Sessions are independent of client
   1.375 +  connections and may be shared by different clients, as long as the internal
   1.376 +  session identifier is known.
   1.377 +
   1.378 +  \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
   1.379 +  int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
   1.380 +  represents a formal theory node status of the PIDE document model. Fields
   1.381 +  \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close> account
   1.382 +  for individual commands within a theory node; \<open>ok\<close> is an abstraction for
   1.383 +  \<open>failed = 0\<close>. The \<open>consolidated\<close> flag indicates whether the outermost theory
   1.384 +  command structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has
   1.385 +  been checked.
   1.386 +\<close>
   1.387 +
   1.388 +
   1.389 +section \<open>Server commands and results\<close>
   1.390 +
   1.391 +text \<open>
   1.392 +  Here follows an overview of particular Isabelle server commands with their
   1.393 +  results, which are usually represented as JSON values with types according
   1.394 +  to \secref{sec:json-types}. The general format of input and output messages
   1.395 +  is described in \secref{sec:input-output-messages}. The relevant
   1.396 +  Isabelle/Scala source files are:
   1.397 +
   1.398 +  \<^medskip>
   1.399 +  \begin{tabular}{l}
   1.400 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
   1.401 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close> \\
   1.402 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/General/json.scala\<close> \\
   1.403 +  \end{tabular}
   1.404 +\<close>
   1.405 +
   1.406 +
   1.407 +subsection \<open>Command \<^verbatim>\<open>help\<close>\<close>
   1.408 +
   1.409 +text \<open>
   1.410 +  \begin{tabular}{ll}
   1.411 +  regular result: & \<^verbatim>\<open>OK\<close> \<open>[string]\<close> \\
   1.412 +  \end{tabular}
   1.413 +  \<^medskip>
   1.414 +
   1.415 +  The \<^verbatim>\<open>help\<close> command has no argument and returns the list of server command
   1.416 +  names. This is occasionally useful for interactive experimentation (see also
   1.417 +  @{tool client} in \secref{sec:tool-client}).
   1.418 +\<close>
   1.419 +
   1.420 +
   1.421 +subsection \<open>Command \<^verbatim>\<open>echo\<close>\<close>
   1.422 +
   1.423 +text \<open>
   1.424 +  \begin{tabular}{ll}
   1.425 +  argument: & \<open>any\<close> \\
   1.426 +  regular result: & \<^verbatim>\<open>OK\<close> \<open>any\<close> \\
   1.427 +  \end{tabular}
   1.428 +  \<^medskip>
   1.429 +
   1.430 +  The \<^verbatim>\<open>echo\<close> command is the identity function: it returns its argument as
   1.431 +  regular result. This is occasionally useful for testing and interactive
   1.432 +  experimentation (see also @{tool client} in \secref{sec:tool-client}).
   1.433 +
   1.434 +  The Scala type of \<^verbatim>\<open>echo\<close> is actually more general than given above:
   1.435 +  \<^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.436 +  be difficult to type on the console in its YXML syntax
   1.437 +  (\secref{sec:yxml-vs-xml}).
   1.438 +\<close>
   1.439 +
   1.440 +
   1.441 +subsection \<open>Command \<^verbatim>\<open>shutdown\<close>\<close>
   1.442 +
   1.443 +text \<open>
   1.444 +  \begin{tabular}{ll}
   1.445 +  regular result: & \<^verbatim>\<open>OK\<close> \\
   1.446 +  \end{tabular}
   1.447 +  \<^medskip>
   1.448 +
   1.449 +  The \<^verbatim>\<open>shutdown\<close> command has no argument and result value. It forces a
   1.450 +  shutdown of the connected server process, stopping all open sessions and
   1.451 +  closing the server socket. This may disrupt pending commands on other
   1.452 +  connections!
   1.453 +
   1.454 +  \<^medskip>
   1.455 +  The command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server connection
   1.456 +  and issues a \<^verbatim>\<open>shutdown\<close> command (see also \secref{sec:tool-server}).
   1.457 +\<close>
   1.458 +
   1.459 +
   1.460 +subsection \<open>Command \<^verbatim>\<open>cancel\<close>\<close>
   1.461 +
   1.462 +text \<open>
   1.463 +  \begin{tabular}{ll}
   1.464 +  argument: & \<open>task\<close> \\
   1.465 +  regular result: & \<^verbatim>\<open>OK\<close> \\
   1.466 +  \end{tabular}
   1.467 +  \<^medskip>
   1.468 +
   1.469 +  The command \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> attempts to cancel the specified
   1.470 +  task.
   1.471 +
   1.472 +  Cancellation is merely a hint that the client prefers an ongoing process to
   1.473 +  be stopped. The command always succeeds formally, but it may get ignored by
   1.474 +  a task that is still running; it might also refer to a non-existing or
   1.475 +  no-longer existing task (without producing an error).
   1.476 +
   1.477 +  Successful cancellation typically leads to an asynchronous failure of type
   1.478 +  \<^verbatim>\<open>FAILED {\<close>\<open>task: uuid, message:\<close>~\<^verbatim>\<open>"Interrupt"}\<close>. A different message is
   1.479 +  also possible, depending how the task handles the event.
   1.480 +\<close>
   1.481 +
   1.482 +
   1.483 +subsection \<open>Command \<^verbatim>\<open>session_build\<close> \label{sec:command-session-build}\<close>
   1.484 +
   1.485 +text \<open>
   1.486 +  \begin{tabular}{lll}
   1.487 +  argument: & \<open>session_build_args\<close> \\
   1.488 +  immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   1.489 +  notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
   1.490 +  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_build_results\<close> \\
   1.491 +  error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_build_results\<close> \\[2ex]
   1.492 +  \end{tabular}
   1.493 +
   1.494 +  \begin{tabular}{lll}
   1.495 +  \<^bold>\<open>type\<close> \<open>session_build_args =\<close> \\
   1.496 +  \quad\<open>{session: string,\<close> \\
   1.497 +  \quad~~\<open>preferences?: string,\<close> & \<^bold>\<open>default:\<close> server preferences \\
   1.498 +  \quad~~\<open>options?: [string],\<close> \\
   1.499 +  \quad~~\<open>dirs?: [string],\<close> \\
   1.500 +  \quad~~\<open>include_sessions: [string],\<close> \\
   1.501 +  \quad~~\<open>system_mode?: bool,\<close> \\
   1.502 +  \quad~~\<open>verbose?: bool}\<close> \\[2ex]
   1.503 +  \end{tabular}
   1.504 +
   1.505 +  \begin{tabular}{ll}
   1.506 +  \<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
   1.507 +  \quad\<open>{session: string,\<close> \\
   1.508 +  \quad~~\<open>ok: bool,\<close> \\
   1.509 +  \quad~~\<open>return_code: int,\<close> \\
   1.510 +  \quad~~\<open>timeout: bool,\<close> \\
   1.511 +  \quad~~\<open>timing: timing}\<close> \\[2ex]
   1.512 +
   1.513 +  \<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
   1.514 +  \quad\<open>{ok: bool,\<close> \\
   1.515 +  \quad~~\<open>return_code: int,\<close> \\
   1.516 +  \quad~~\<open>sessions: [session_build_result]}\<close> \\
   1.517 +  \end{tabular}
   1.518 +\<close>
   1.519 +
   1.520 +text \<open>
   1.521 +  The \<^verbatim>\<open>session_build\<close> command prepares a session image for interactive use of
   1.522 +  theories. This is a limited version of command-line tool @{tool build}
   1.523 +  (\secref{sec:tool-build}), with specific options to request a formal context
   1.524 +  for an interactive PIDE session.
   1.525 +
   1.526 +  The build process is asynchronous, with notifications that inform about the
   1.527 +  progress of loaded theories. Some further informative messages are output as
   1.528 +  well.
   1.529 +
   1.530 +  Coordination of independent build processes is at the discretion of the
   1.531 +  client (or end-user), just as for @{tool build} and @{tool jedit}. There is
   1.532 +  no built-in coordination of conflicting builds with overlapping hierarchies
   1.533 +  of session images. In the worst case, a session image produced by one task
   1.534 +  may get overwritten by another task!
   1.535 +\<close>
   1.536 +
   1.537 +
   1.538 +subsubsection \<open>Arguments\<close>
   1.539 +
   1.540 +text \<open>
   1.541 +  The \<open>session\<close> field specifies the target session name. The build process
   1.542 +  will produce all required ancestor images according to the overall session
   1.543 +  graph.
   1.544 +
   1.545 +  \<^medskip>
   1.546 +  The environment of Isabelle system options is determined from \<open>preferences\<close>
   1.547 +  that are augmented by \<open>options\<close>, which is a list individual updates of the
   1.548 +  form the \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> (the latter abbreviates
   1.549 +  \<open>name\<close>\<^verbatim>\<open>=true\<close>); see also command-line option \<^verbatim>\<open>-o\<close> for @{tool build}. The
   1.550 +  preferences are loaded from the file
   1.551 +  \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> by default, but the client may
   1.552 +  provide alternative contents for it (as text, not a file-name). This could
   1.553 +  be relevant in situations where client and server run in different
   1.554 +  operating-system contexts.
   1.555 +
   1.556 +  \<^medskip>
   1.557 +  The \<open>dirs\<close> field specifies additional directories for session ROOT and ROOTS
   1.558 +  files (\secref{sec:session-root}). This augments the name space of available
   1.559 +  sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
   1.560 +
   1.561 +  \<^medskip>
   1.562 +  The \<open>include_sessions\<close> field specifies sessions whose theories should be
   1.563 +  included in the overall name space of session-qualified theory names. This
   1.564 +  corresponds to a \<^bold>\<open>sessions\<close> specification in ROOT files
   1.565 +  (\secref{sec:session-root}). It enables the \<^verbatim>\<open>use_theories\<close> command
   1.566 +  (\secref{sec:command-use-theories}) to refer to sources from other sessions
   1.567 +  in a robust manner, instead of relying on directory locations.
   1.568 +
   1.569 +  \<^medskip>
   1.570 +  The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
   1.571 +  log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
   1.572 +  @{setting ISABELLE_OUTPUT} (which is normally in @{setting
   1.573 +  ISABELLE_HOME_USER}). See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
   1.574 +
   1.575 +  \<^medskip>
   1.576 +  The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
   1.577 +  similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
   1.578 +\<close>
   1.579 +
   1.580 +
   1.581 +subsubsection \<open>Intermediate output\<close>
   1.582 +
   1.583 +text \<open>
   1.584 +  The asynchronous notifications of command \<^verbatim>\<open>session_build\<close> mainly serve as
   1.585 +  progress indicator: the output resembles that of the session build window of
   1.586 +  Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
   1.587 +
   1.588 +  For the client it is usually sufficient to print the messages in plain text,
   1.589 +  but note that \<open>theory_progress\<close> also reveals formal \<open>theory\<close> and
   1.590 +  \<open>session\<close> names directly.
   1.591 +\<close>
   1.592 +
   1.593 +
   1.594 +subsubsection \<open>Results\<close>
   1.595 +
   1.596 +text \<open>
   1.597 +  The overall \<open>session_build_results\<close> contain both a summary and an entry
   1.598 +  \<open>session_build_result\<close> for each session in the build hierarchy. The result
   1.599 +  is always provided, independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or
   1.600 +  failure (\<^verbatim>\<open>FAILED\<close> task).
   1.601 +
   1.602 +  The \<open>ok\<close> field tells abstractly, whether all required session builds came
   1.603 +  out as \<open>ok\<close>, i.e.\ with zero \<open>return_code\<close>. A non-zero \<open>return_code\<close>
   1.604 +  indicates an error according to usual POSIX conventions for process exit.
   1.605 +
   1.606 +  The individual \<open>session_build_result\<close> entries provide extra fields:
   1.607 +
   1.608 +  \<^item> \<open>timeout\<close> tells if the build process was aborted after running too long,
   1.609 +
   1.610 +  \<^item> \<open>timing\<close> gives the overall process timing in the usual Isabelle format
   1.611 +  with elapsed, CPU, GC time.
   1.612 +\<close>
   1.613 +
   1.614 +
   1.615 +subsubsection \<open>Examples\<close>
   1.616 +
   1.617 +text \<open>
   1.618 +  Build of a session image from the Isabelle distribution:
   1.619 +  @{verbatim [display] \<open>session_build {"session": "HOL-Word"}\<close>}
   1.620 +
   1.621 +  Build a session image from the Archive of Formal Proofs:
   1.622 +  @{verbatim [display] \<open>session_build {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
   1.623 +\<close>
   1.624 +
   1.625 +
   1.626 +subsection \<open>Command \<^verbatim>\<open>session_start\<close> \label{sec:command-session-start}\<close>
   1.627 +
   1.628 +text \<open>
   1.629 +  \begin{tabular}{lll}
   1.630 +  argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\
   1.631 +  immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   1.632 +  notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
   1.633 +  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id \<oplus> {tmp_dir: string}\<close> \\
   1.634 +  error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex]
   1.635 +  \end{tabular}
   1.636 +
   1.637 +  \<^medskip>
   1.638 +  The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with
   1.639 +  underlying Isabelle/ML process, based on a session image that it produces on
   1.640 +  demand using \<^verbatim>\<open>session_build\<close>. Thus it accepts all \<open>session_build_args\<close> and
   1.641 +  produces similar notifications, but the detailed \<open>session_build_results\<close> are
   1.642 +  omitted.
   1.643 +
   1.644 +  The session build and startup process is asynchronous: when the task is
   1.645 +  finished, the session remains active for commands, until a \<^verbatim>\<open>session_stop\<close>
   1.646 +  or \<^verbatim>\<open>shutdown\<close> command is sent to the server.
   1.647 +
   1.648 +  Sessions are independent of client connections: it is possible to start a
   1.649 +  session and later apply \<^verbatim>\<open>use_theories\<close> on different connections, as long as
   1.650 +  the internal session identifier is known: shared theory imports will be used
   1.651 +  only once (and persist until purged explicitly).
   1.652 +\<close>
   1.653 +
   1.654 +
   1.655 +subsubsection \<open>Arguments\<close>
   1.656 +
   1.657 +text \<open>
   1.658 +  Most arguments are shared with \<^verbatim>\<open>session_build\<close>
   1.659 +  (\secref{sec:command-session-build}).
   1.660 +
   1.661 +  \<^medskip>
   1.662 +  The \<open>print_mode\<close> field adds identifiers of print modes to be made active for
   1.663 +  this session. For example, \<^verbatim>\<open>"print_mode": ["ASCII"]\<close> prefers ASCII
   1.664 +  replacement syntax over mathematical Isabelle symbols. See also option \<^verbatim>\<open>-m\<close>
   1.665 +  in @{tool process} (\secref{sec:tool-process}).
   1.666 +\<close>
   1.667 +
   1.668 +
   1.669 +subsubsection \<open>Results\<close>
   1.670 +
   1.671 +text \<open>
   1.672 +  The \<open>session_id\<close> provides the internal identification of the session object
   1.673 +  within the sever process. It can remain active as long as the server is
   1.674 +  running, independently of the current client connection.
   1.675 +
   1.676 +  \<^medskip>
   1.677 +  The \<open>tmp_dir\<close> fields reveals a temporary directory that is specifically
   1.678 +  created for this session and deleted after it has been stopped. This may
   1.679 +  serve as auxiliary file-space for the \<^verbatim>\<open>use_theories\<close> command, but
   1.680 +  concurrent use requires some care in naming temporary files, e.g.\ by
   1.681 +  using sub-directories with globally unique names.
   1.682 +\<close>
   1.683 +
   1.684 +
   1.685 +subsection \<open>Examples\<close>
   1.686 +
   1.687 +text \<open>
   1.688 +  Start a default Isabelle/HOL session:
   1.689 +  @{verbatim [display] \<open>session_start {"session": "HOL"}\<close>}
   1.690 +
   1.691 +  Start a session from the Archive of Formal Proofs:
   1.692 +  @{verbatim [display] \<open>session_start {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
   1.693 +\<close>
   1.694 +
   1.695 +
   1.696 +subsection \<open>Command \<^verbatim>\<open>session_stop\<close>\<close>
   1.697 +
   1.698 +text \<open>
   1.699 +  \begin{tabular}{ll}
   1.700 +  argument: & \<open>session_id\<close> \\
   1.701 +  immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   1.702 +  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_stop_result\<close> \\
   1.703 +  error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_stop_result\<close> \\[2ex]
   1.704 +  \end{tabular}
   1.705 +
   1.706 +  \begin{tabular}{l}
   1.707 +  \<^bold>\<open>type\<close> \<open>session_stop_result = {ok: bool, return_code: int}\<close>
   1.708 +  \end{tabular}
   1.709 +
   1.710 +  \<^medskip>
   1.711 +  The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified PIDE
   1.712 +  session. This asynchronous tasks usually finishes quickly. Failure only
   1.713 +  happens in unusual situations, according to the return code of the
   1.714 +  underlying Isabelle/ML process.
   1.715 +\<close>
   1.716 +
   1.717 +
   1.718 +subsubsection \<open>Arguments\<close>
   1.719 +
   1.720 +text \<open>
   1.721 +  The \<open>session_id\<close> provides the UUID originally created by the server for this
   1.722 +  session.
   1.723 +\<close>
   1.724 +
   1.725 +
   1.726 +subsubsection \<open>Results\<close>
   1.727 +
   1.728 +text \<open>
   1.729 +  The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process has
   1.730 +  terminated properly.
   1.731 +
   1.732 +  The \<open>return_code\<close> field expresses this information according to usual POSIX
   1.733 +  conventions for process exit.
   1.734 +\<close>
   1.735 +
   1.736 +
   1.737 +subsection \<open>Command \<^verbatim>\<open>use_theories\<close> \label{sec:command-use-theories}\<close>
   1.738 +
   1.739 +text \<open>
   1.740 +  \begin{tabular}{ll}
   1.741 +  argument: & \<open>use_theories_arguments\<close> \\
   1.742 +  regular result: & \<^verbatim>\<open>OK\<close> \<open>use_theories_results\<close> \\
   1.743 +  \end{tabular}
   1.744 +
   1.745 +  \begin{tabular}{ll}
   1.746 +  \<^bold>\<open>type\<close> \<open>theory_name = string | {name: string, pos: position}\<close> \\
   1.747 +  \end{tabular}
   1.748 +
   1.749 +  \begin{tabular}{ll}
   1.750 +  \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
   1.751 +  \quad\<open>{session_id: uuid,\<close> \\
   1.752 +  \quad~~\<open>theories: [theory_name],\<close> \\
   1.753 +  \quad~~\<open>qualifier?: string,\<close> \\
   1.754 +  \quad~~\<open>master_dir?: string,\<close> \\
   1.755 +  \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   1.756 +  \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
   1.757 +  \end{tabular}
   1.758 +
   1.759 +  \begin{tabular}{ll}
   1.760 +  \<^bold>\<open>type\<close> \<open>node_result =\<close> \\
   1.761 +  \quad\<open>{node_name: string,\<close> \\
   1.762 +  \quad~~\<open>theory: string,\<close> \\
   1.763 +  \quad~~\<open>status: node_status,\<close> \\
   1.764 +  \quad~~\<open>messages: [message]}\<close> \\[2ex]
   1.765 +
   1.766 +  \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
   1.767 +  \quad\<open>{ok: bool,\<close> \\
   1.768 +  \quad~~\<open>errors: [message],\<close> \\
   1.769 +  \quad~~\<open>nodes: [node_result]}\<close> \\[2ex]
   1.770 +  \end{tabular}
   1.771 +
   1.772 +  \<^medskip>
   1.773 +  The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
   1.774 +  current version of theory files to it, while dependencies are resolved
   1.775 +  implicitly. The command succeeds eventually, when all theories have been
   1.776 +  \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
   1.777 +  (\secref{sec:json-types}): the outermost command structure has finished (or
   1.778 +  failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
   1.779 +
   1.780 +  Already used theories persist in the session until purged explicitly. This
   1.781 +  also means that repeated invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it
   1.782 +  could make sense to do that with different values for \<open>pretty_margin\<close> or
   1.783 +  \<open>unicode_symbols\<close> to get different formatting for \<open>errors\<close> or \<open>messages\<close>.
   1.784 +\<close>
   1.785 +
   1.786 +
   1.787 +subsubsection \<open>Arguments\<close>
   1.788 +
   1.789 +text \<open>
   1.790 +  The \<open>session_id\<close> is the identifier provided by the server, when the session
   1.791 +  was created (possibly on a different client connection).
   1.792 +
   1.793 +  \<^medskip>
   1.794 +  The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
   1.795 +  ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
   1.796 +  specifications may be given, which is occasionally useful for precise error
   1.797 +  locations.
   1.798 +
   1.799 +  \<^medskip>
   1.800 +  The \<open>qualifier\<close> field provides an alternative session qualifier for theories
   1.801 +  that are not formally recognized as a member of a particular session. The
   1.802 +  default is \<^verbatim>\<open>Draft\<close> as in Isabelle/jEdit. There is rarely a need to change
   1.803 +  that, as theory nodes are already uniquely identified by their physical
   1.804 +  file-system location. This already allows reuse of theory base names with
   1.805 +  the same session qualifier --- as long as these theories are not used
   1.806 +  together (e.g.\ in \<^theory_text>\<open>imports\<close>).
   1.807 +
   1.808 +  \<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
   1.809 +  the imported theory. Normally this is determined implicitly from the parent
   1.810 +  directory of the theory file.
   1.811 +
   1.812 +  \<^medskip>
   1.813 +  The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
   1.814 +  default is suitable for classic console output. Formatting happens at the
   1.815 +  end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.
   1.816 +
   1.817 +  \<^medskip>
   1.818 +  The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> renders message output for direct
   1.819 +  output on a Unicode capable channel, ideally with the Isabelle fonts as in
   1.820 +  Isabelle/jEdit. The default is to keep the symbolic representation of
   1.821 +  Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead of its rendering as \<open>\<forall>\<close>. This means the
   1.822 +  client needs to perform its own rendering before presenting it to the
   1.823 +  end-user.
   1.824 +\<close>
   1.825 +
   1.826 +
   1.827 +subsubsection \<open>Results\<close>
   1.828 +
   1.829 +text \<open>
   1.830 +  The \<open>ok\<close> field indicates overall success of processing the specified
   1.831 +  theories with all their dependencies.
   1.832 +
   1.833 +  When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively
   1.834 +  (including imported theories). The messages contain position information for
   1.835 +  the original theory nodes.
   1.836 +
   1.837 +  \<^medskip>
   1.838 +  The \<open>nodes\<close> field provides detailed information about each imported theory
   1.839 +  node. The individual fields are as follows:
   1.840 +
   1.841 +  \<^item> \<open>node_name\<close>: the physical name for the theory node, based on its
   1.842 +  file-system location;
   1.843 +
   1.844 +  \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close>;
   1.845 +
   1.846 +  \<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
   1.847 +  \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
   1.848 +
   1.849 +  \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
   1.850 +  (\<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>, etc.).
   1.851 +\<close>
   1.852 +
   1.853 +
   1.854 +subsubsection \<open>Examples\<close>
   1.855 +
   1.856 +text \<open>
   1.857 +  Process some example theory from the Isabelle distribution, within the
   1.858 +  context of an already started session for Isabelle/HOL (see also
   1.859 +  \secref{sec:command-session-start}):
   1.860 +  @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Isar_Examples/Drinker"]}\<close>}
   1.861 +
   1.862 +  \<^medskip>
   1.863 +  Process some example theories in the context of their (single) parent
   1.864 +  session:
   1.865 +
   1.866 +  @{verbatim [display] \<open>session_start {"session": "HOL-Library"}
   1.867 +use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
   1.868 +session_stop {"session_id": ...}\<close>}
   1.869 +
   1.870 +  \<^medskip>
   1.871 +  Process some example theories that import other theories via
   1.872 +  session-qualified theory names:
   1.873 +
   1.874 +  @{verbatim [display] \<open>session_start {"session": "HOL", "include_sessions": ["HOL-Unix"]}
   1.875 +use_theories {"session_id": ..., "theories": ["HOL-Unix.Unix"]}
   1.876 +session_stop {"session_id": ...}\<close>}
   1.877  \<close>
   1.878  
   1.879  end
     2.1 --- a/src/Pure/PIDE/protocol.scala	Thu Mar 22 13:53:15 2018 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Mar 22 17:06:15 2018 +0100
     2.3 @@ -144,13 +144,13 @@
     2.4    sealed case class Node_Status(
     2.5      unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
     2.6    {
     2.7 +    def ok: Boolean = failed == 0
     2.8      def total: Int = unprocessed + running + warned + failed + finished
     2.9 -    def ok: Boolean = failed == 0
    2.10  
    2.11      def json: JSON.Object.T =
    2.12 -      JSON.Object("unprocessed" -> unprocessed, "running" -> running, "warned" -> warned,
    2.13 -        "failed" -> failed, "finished" -> finished, "consolidated" -> consolidated,
    2.14 -        "total" -> total, "ok" -> ok)
    2.15 +      JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
    2.16 +        "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
    2.17 +        "consolidated" -> consolidated)
    2.18    }
    2.19  
    2.20    def node_status(
    2.21 @@ -239,6 +239,13 @@
    2.22        case _ => false
    2.23      }
    2.24  
    2.25 +  def is_writeln(msg: XML.Tree): Boolean =
    2.26 +    msg match {
    2.27 +      case XML.Elem(Markup(Markup.WRITELN, _), _) => true
    2.28 +      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true
    2.29 +      case _ => false
    2.30 +    }
    2.31 +
    2.32    def is_warning(msg: XML.Tree): Boolean =
    2.33      msg match {
    2.34        case XML.Elem(Markup(Markup.WARNING, _), _) => true
    2.35 @@ -263,6 +270,9 @@
    2.36    def is_inlined(msg: XML.Tree): Boolean =
    2.37      !(is_result(msg) || is_tracing(msg) || is_state(msg))
    2.38  
    2.39 +  def is_exported(msg: XML.Tree): Boolean =
    2.40 +    is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
    2.41 +
    2.42  
    2.43    /* breakpoints */
    2.44  
     3.1 --- a/src/Pure/System/isabelle_system.scala	Thu Mar 22 13:53:15 2018 +0100
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Mar 22 17:06:15 2018 +0100
     3.3 @@ -173,10 +173,10 @@
     3.4      File.platform_file(path)
     3.5    }
     3.6  
     3.7 -  def tmp_file(name: String, ext: String = ""): JFile =
     3.8 +  def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile =
     3.9    {
    3.10      val suffix = if (ext == "") "" else "." + ext
    3.11 -    val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile
    3.12 +    val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
    3.13      file.deleteOnExit
    3.14      file
    3.15    }
    3.16 @@ -217,9 +217,9 @@
    3.17      }
    3.18    }
    3.19  
    3.20 -  def tmp_dir(name: String): JFile =
    3.21 +  def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
    3.22    {
    3.23 -    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
    3.24 +    val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
    3.25      dir.deleteOnExit
    3.26      dir
    3.27    }
     4.1 --- a/src/Pure/Thy/sessions.scala	Thu Mar 22 13:53:15 2018 +0100
     4.2 +++ b/src/Pure/Thy/sessions.scala	Thu Mar 22 17:06:15 2018 +0100
     4.3 @@ -373,6 +373,7 @@
     4.4      session: String,
     4.5      progress: Progress = No_Progress,
     4.6      dirs: List[Path] = Nil,
     4.7 +    include_sessions: List[String] = Nil,
     4.8      ancestor_session: Option[String] = None,
     4.9      all_known: Boolean = false,
    4.10      focus_session: Boolean = false,
    4.11 @@ -435,15 +436,17 @@
    4.12        if (infos1.isEmpty) full_sessions
    4.13        else load_structure(options, dirs = dirs, infos = infos1)
    4.14  
    4.15 -    val select_sessions1 =
    4.16 -      if (focus_session) full_sessions1.imports_descendants(List(session1))
    4.17 -      else List(session1)
    4.18      val selected_sessions1 =
    4.19 +    {
    4.20 +      val sel_sessions1 = session1 :: include_sessions
    4.21 +      val select_sessions1 =
    4.22 +        if (focus_session) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
    4.23        full_sessions1.selection(Selection(sessions = select_sessions1))
    4.24 +    }
    4.25  
    4.26      val sessions1 = if (all_known) full_sessions1 else selected_sessions1
    4.27      val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)
    4.28 -    val base1 = if (all_known) deps1(session1).copy(known = deps1.all_known) else deps1(session1)
    4.29 +    val base1 = deps1(session1).copy(known = deps1.all_known)
    4.30  
    4.31      Base_Info(options, dirs, session1, sessions1, deps1.errors, base1, infos1)
    4.32    }
     5.1 --- a/src/Pure/Thy/thy_resources.scala	Thu Mar 22 13:53:15 2018 +0100
     5.2 +++ b/src/Pure/Thy/thy_resources.scala	Thu Mar 22 17:06:15 2018 +0100
     5.3 @@ -7,6 +7,9 @@
     5.4  package isabelle
     5.5  
     5.6  
     5.7 +import java.io.{File => JFile}
     5.8 +
     5.9 +
    5.10  object Thy_Resources
    5.11  {
    5.12    /* PIDE session */
    5.13 @@ -65,7 +68,6 @@
    5.14            Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
    5.15          pos = command.span.keyword_pos(start).position(command.span.name)
    5.16          (_, tree) <- state.command_results(version, command).iterator
    5.17 -        if Protocol.is_inlined(tree)
    5.18         } yield (tree, pos)).toList
    5.19      }
    5.20    }
    5.21 @@ -76,6 +78,14 @@
    5.22    {
    5.23      session =>
    5.24  
    5.25 +    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
    5.26 +
    5.27 +    override def stop(): Process_Result =
    5.28 +    {
    5.29 +      try { super.stop() }
    5.30 +      finally { Isabelle_System.rm_tree(tmp_dir) }
    5.31 +    }
    5.32 +
    5.33      def use_theories(
    5.34        theories: List[(String, Position.T)],
    5.35        qualifier: String = Sessions.DRAFT,
     6.1 --- a/src/Pure/Tools/server.scala	Thu Mar 22 13:53:15 2018 +0100
     6.2 +++ b/src/Pure/Tools/server.scala	Thu Mar 22 17:06:15 2018 +0100
     6.3 @@ -69,7 +69,8 @@
     6.4          "help" -> { case (_, ()) => table.keySet.toList.sorted },
     6.5          "echo" -> { case (_, t) => t },
     6.6          "shutdown" -> { case (context, ()) => context.server.shutdown() },
     6.7 -        "cancel" -> { case (context, JSON.Value.UUID(id)) => context.cancel_task(id) },
     6.8 +        "cancel" ->
     6.9 +          { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) },
    6.10          "session_build" ->
    6.11            { case (context, Server_Commands.Session_Build(args)) =>
    6.12                context.make_task(task =>
    6.13 @@ -115,8 +116,8 @@
    6.14  
    6.15    def json_error(exn: Throwable): JSON.Object.T =
    6.16      exn match {
    6.17 +      case e: Error => Reply.error_message(e.message) ++ e.json
    6.18        case ERROR(msg) => Reply.error_message(msg)
    6.19 -      case e: Error => Reply.error_message(e.message) ++ e.json
    6.20        case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
    6.21        case _ => JSON.Object.empty
    6.22      }
    6.23 @@ -130,7 +131,7 @@
    6.24        else JSON.Object(Markup.KIND -> kind, "message" -> msg)
    6.25  
    6.26      def error_message(msg: String): JSON.Object.T =
    6.27 -      message(msg, kind = Markup.ERROR_MESSAGE)
    6.28 +      message(msg, kind = Markup.ERROR)
    6.29  
    6.30      def unapply(msg: String): Option[(Reply.Value, Any)] =
    6.31      {
    6.32 @@ -225,7 +226,7 @@
    6.33      def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
    6.34      def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
    6.35      def error_message(msg: String, more: JSON.Object.Entry*): Unit =
    6.36 -      message(Markup.ERROR_MESSAGE, msg, more:_*)
    6.37 +      message(Markup.ERROR, msg, more:_*)
    6.38  
    6.39      def progress(more: JSON.Object.Entry*): Connection_Progress =
    6.40        new Connection_Progress(context, more:_*)
     7.1 --- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 13:53:15 2018 +0100
     7.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 17:06:15 2018 +0100
     7.3 @@ -23,6 +23,16 @@
     7.4        case _ => None
     7.5      }
     7.6  
     7.7 +  object Cancel
     7.8 +  {
     7.9 +    sealed case class Args(task: UUID)
    7.10 +
    7.11 +    def unapply(json: JSON.T): Option[Args] =
    7.12 +      for { task <- JSON.uuid(json, "task") }
    7.13 +      yield Args(task)
    7.14 +  }
    7.15 +
    7.16 +
    7.17    object Session_Build
    7.18    {
    7.19      sealed case class Args(
    7.20 @@ -30,10 +40,7 @@
    7.21        preferences: String = default_preferences,
    7.22        options: List[String] = Nil,
    7.23        dirs: List[String] = Nil,
    7.24 -      ancestor_session: String = "",
    7.25 -      all_known: Boolean = false,
    7.26 -      focus_session: Boolean = false,
    7.27 -      required_session: Boolean = false,
    7.28 +      include_sessions: List[String] = Nil,
    7.29        system_mode: Boolean = false,
    7.30        verbose: Boolean = false)
    7.31  
    7.32 @@ -43,17 +50,13 @@
    7.33          preferences <- JSON.string_default(json, "preferences", default_preferences)
    7.34          options <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
    7.35          dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
    7.36 -        ancestor_session <- JSON.string_default(json, "ancestor_session")
    7.37 -        all_known <- JSON.bool_default(json, "all_known")
    7.38 -        focus_session <- JSON.bool_default(json, "focus_session")
    7.39 -        required_session <- JSON.bool_default(json, "required_session")
    7.40 +        include_sessions <- JSON.list_default(json, "include_sessions", JSON.Value.String.unapply _)
    7.41          system_mode <- JSON.bool_default(json, "system_mode")
    7.42          verbose <- JSON.bool_default(json, "verbose")
    7.43        }
    7.44        yield {
    7.45          Args(session, preferences = preferences, options = options, dirs = dirs,
    7.46 -          ancestor_session = ancestor_session, all_known = all_known, focus_session = focus_session,
    7.47 -          required_session = required_session, system_mode = system_mode, verbose = verbose)
    7.48 +          include_sessions = include_sessions, system_mode = system_mode, verbose = verbose)
    7.49        }
    7.50  
    7.51      def command(args: Args, progress: Progress = No_Progress)
    7.52 @@ -63,14 +66,8 @@
    7.53        val dirs = args.dirs.map(Path.explode(_))
    7.54  
    7.55        val base_info =
    7.56 -        Sessions.base_info(options,
    7.57 -          args.session,
    7.58 -          progress = progress,
    7.59 -          dirs = dirs,
    7.60 -          ancestor_session = proper_string(args.ancestor_session),
    7.61 -          all_known = args.all_known,
    7.62 -          focus_session = args.focus_session,
    7.63 -          required_session = args.required_session)
    7.64 +        Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
    7.65 +          include_sessions = args.include_sessions)
    7.66        val base = base_info.check_base
    7.67  
    7.68        val results =
    7.69 @@ -89,14 +86,19 @@
    7.70  
    7.71        val results_json =
    7.72          JSON.Object(
    7.73 +          "ok" -> results.ok,
    7.74            "return_code" -> results.rc,
    7.75            "sessions" ->
    7.76              results.sessions.toList.sortBy(sessions_order).map(session =>
    7.77 -              JSON.Object(
    7.78 -                "session" -> session,
    7.79 -                "return_code" -> results(session).rc,
    7.80 -                "timeout" -> results(session).timeout,
    7.81 -                "timing" -> results(session).timing.json)))
    7.82 +              {
    7.83 +                val result = results(session)
    7.84 +                JSON.Object(
    7.85 +                  "session" -> session,
    7.86 +                  "ok" -> result.ok,
    7.87 +                  "return_code" -> result.rc,
    7.88 +                  "timeout" -> result.timeout,
    7.89 +                  "timing" -> result.timing.json)
    7.90 +              }))
    7.91  
    7.92        if (results.ok) (results_json, results, base_info)
    7.93        else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
    7.94 @@ -119,7 +121,9 @@
    7.95      def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
    7.96        : (JSON.Object.T, (UUID, Thy_Resources.Session)) =
    7.97      {
    7.98 -      val base_info = Session_Build.command(args.build, progress = progress)._3
    7.99 +      val base_info =
   7.100 +        try { Session_Build.command(args.build, progress = progress)._3 }
   7.101 +        catch { case exn: Server.Error => error(exn.message) }
   7.102  
   7.103        val session =
   7.104          Thy_Resources.start_session(
   7.105 @@ -132,7 +136,11 @@
   7.106            log = log)
   7.107  
   7.108        val id = UUID()
   7.109 -      val res = JSON.Object("session_name" -> base_info.session, "session_id" -> id.toString)
   7.110 +
   7.111 +      val res =
   7.112 +        JSON.Object(
   7.113 +          "session_id" -> id.toString,
   7.114 +          "tmp_dir" -> File.path(session.tmp_dir).implode)
   7.115  
   7.116        (res, id -> session)
   7.117      }
   7.118 @@ -146,7 +154,7 @@
   7.119      def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
   7.120      {
   7.121        val result = session.stop()
   7.122 -      val result_json = JSON.Object("return_code" -> result.rc)
   7.123 +      val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
   7.124  
   7.125        if (result.ok) (result_json, result)
   7.126        else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)
   7.127 @@ -196,7 +204,9 @@
   7.128            case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
   7.129            case elem: XML.Elem =>
   7.130              val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
   7.131 -            val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => a })
   7.132 +            val kind =
   7.133 +              Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
   7.134 +                if (Protocol.is_legacy(elem)) Markup.WARNING else a })
   7.135              Server.Reply.message(output_text(msg), kind = kind getOrElse "") + position
   7.136          }
   7.137        }
   7.138 @@ -208,6 +218,7 @@
   7.139              (for {
   7.140                (name, status) <- result.nodes if !status.ok
   7.141                (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
   7.142 +              if Protocol.is_exported(tree)
   7.143              } yield output_message(tree, pos)),
   7.144            "nodes" ->
   7.145              (for ((name, status) <- result.nodes) yield