more documentation;
authorwenzelm
Wed Mar 21 21:50:28 2018 +0100 (14 months ago)
changeset 67917d13b2dd20f5e
parent 67916 a72f01c63262
child 67918 7dc204623770
more documentation;
src/Doc/System/Server.thy
     1.1 --- a/src/Doc/System/Server.thy	Wed Mar 21 21:31:40 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Wed Mar 21 21:50:28 2018 +0100
     1.3 @@ -224,7 +224,7 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 -subsection \<open>Input and output messages\<close>
     1.8 +subsection \<open>Input and output messages \label{sec:input-output-messages}\<close>
     1.9  
    1.10  text \<open>
    1.11    Server input and output messages have a uniform format as follows:
    1.12 @@ -346,9 +346,677 @@
    1.13    asynchronous messages properly.
    1.14  
    1.15    The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
    1.16 -  prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result with error message
    1.17 -  \<^verbatim>\<open>Interrupt\<close>, but this is not guaranteed: the cancel event may come too
    1.18 -  late or the task may just ignore it.
    1.19 +  prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is not guaranteed:
    1.20 +  the cancel event may come too late or the task may just ignore it.
    1.21 +\<close>
    1.22 +
    1.23 +
    1.24 +section \<open>Server commands and results\<close>
    1.25 +
    1.26 +text \<open>
    1.27 +  Here follows an overview of particular Isabelle server commands with their
    1.28 +  results, which are usually represented as JSON values. The general format of
    1.29 +  input and output messages is described in
    1.30 +  \secref{sec:input-output-messages}. The relevant Isabelle/Scala source files
    1.31 +  are:
    1.32 +
    1.33 +  \<^medskip>
    1.34 +  \begin{tabular}{l}
    1.35 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
    1.36 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close>
    1.37 +  \end{tabular}
    1.38 +\<close>
    1.39 +
    1.40 +
    1.41 +subsection \<open>Types for JSON values\<close>
    1.42 +
    1.43 +text \<open>
    1.44 +  In order to specify concrete JSON types for command arguments and result
    1.45 +  messages, the following type definition language shall be used:
    1.46 +
    1.47 +  \<^rail>\<open>
    1.48 +    @{syntax type_def}: @'type' @{syntax name} '=' @{syntax type}
    1.49 +    ;
    1.50 +    @{syntax type}: @{syntax name} | @{syntax value} | 'any' | 'null' |
    1.51 +      'bool' | 'int' | 'long' | 'double' | 'string' | '[' @{syntax type} ']' |
    1.52 +      '{' (@{syntax field_type} ',' *) '}' |
    1.53 +      @{syntax type} '\<oplus>' @{syntax type} |
    1.54 +      @{syntax type} '|' @{syntax type}
    1.55 +    ;
    1.56 +    @{syntax field_type}: @{syntax name} ('?'?) ':' @{syntax type}
    1.57 +  \<close>
    1.58 +
    1.59 +  This is a simplified version of interfaces in
    1.60 +  TypeScript.\<^footnote>\<open>\<^url>\<open>https://www.typescriptlang.org/docs/handbook/interfaces.html\<close>\<close>
    1.61 +  The meaning of these types is specified wrt. the implementation in
    1.62 +  Isabelle/Scala as follows.
    1.63 +
    1.64 +  \<^item> A \<open>name\<close> refers to a type defined elsewhere. The environment of type
    1.65 +  definitions is given informally: put into proper foundational order, it
    1.66 +  needs to specify a strongly normalizing system; type definitions may not be
    1.67 +  recursive.
    1.68 +
    1.69 +  \<^item> A \<open>value\<close> in JSON notation represents the singleton type of the given
    1.70 +  item. For example, the string \<^verbatim>\<open>"error"\<close> can be used is the type for a slot
    1.71 +  that is guaranteed to contain that constant.
    1.72 +
    1.73 +  \<^item> Type \<open>any\<close> is the super type of all other types: it is an untyped slot in
    1.74 +  the specification and corresponds to \<^verbatim>\<open>Any\<close> or \<^verbatim>\<open>JSON.T\<close> in Isabelle/Scala.
    1.75 +
    1.76 +  \<^item> Type \<open>null\<close> is the type of the improper value \<open>null\<close>; it corresponds to
    1.77 +  type \<^verbatim>\<open>Null\<close> in Scala and is normally not used in Isabelle/Scala.\<^footnote>\<open>See also
    1.78 +  ``Null References: The Billion Dollar Mistake'' by Tony Hoare
    1.79 +  \<^url>\<open>https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare\<close>.\<close>
    1.80 +
    1.81 +  \<^item> Type \<open>bool\<close> is the type of the truth values \<open>true\<close> and \<open>false\<close>; it
    1.82 +  corresponds to \<^verbatim>\<open>Boolean\<close> in Scala.
    1.83 +
    1.84 +  \<^item> Types \<open>int\<close>, \<open>long\<close>, \<open>double\<close> are specific versions of the generic
    1.85 +  \<open>number\<close> type, corresponding to \<^verbatim>\<open>Int\<close>, \<^verbatim>\<open>Long\<close>, \<^verbatim>\<open>Double\<close> in Scala, but
    1.86 +  \<^verbatim>\<open>Long\<close> is limited to 53 bit precision.\<^footnote>\<open>Implementations of JSON typically
    1.87 +  standardize \<open>number\<close> to \<^verbatim>\<open>Double\<close>, which can absorb \<^verbatim>\<open>Int\<close> faithfully, but
    1.88 +  not all of \<^verbatim>\<open>Long\<close>.\<close>
    1.89 +
    1.90 +  \<^item> Type \<open>string\<close> represents Unicode text; it corresponds to type \<^verbatim>\<open>String\<close> in
    1.91 +  Scala.
    1.92 +
    1.93 +  \<^item> Type \<open>[t]\<close> is the array (or list) type over \<open>t\<close>; it corresponds to
    1.94 +  \<^verbatim>\<open>List[t]\<close> in Scala. The list type is co-variant as usual (i.e.\ monotonic
    1.95 +  wrt. the subtype order).
    1.96 +
    1.97 +  \<^item> Object types describe the possible content of JSON records, with field
    1.98 +  names and types. A question mark after a field name means that it is
    1.99 +  optional: in Scala this could refer to an explicit type \<^verbatim>\<open>Option[t]\<close>. For
   1.100 +  example, \<open>{a: int, b?: string}\<close> corresponds to a Scala case class with
   1.101 +  arguments \<^verbatim>\<open>a: Int\<close>, \<^verbatim>\<open>b: Option[String]\<close>.
   1.102 +
   1.103 +  Alternatively, optional fields can have a default value. If nothing else is
   1.104 +  specified, the standard default value is the ``empty'' value of a type,
   1.105 +  i.e.\ \<^verbatim>\<open>0\<close> for the number types, \<^verbatim>\<open>false\<close> for \<open>bool\<close>, or the empty string,
   1.106 +  array, object etc.
   1.107 +
   1.108 +  Object types are \<^emph>\<open>permissive\<close> in the sense that only the specified field
   1.109 +  names need to conform to the given types, but unspecified fields may be
   1.110 +  present as well.
   1.111 +
   1.112 +  \<^item> The type expression \<open>t\<^sub>1 \<oplus> t\<^sub>2\<close> only works for two object types with
   1.113 +  disjoint field names: it is the concatenation of the respective @{syntax
   1.114 +  field_type} specifications taken together. For example: \<open>{task: string} \<oplus>
   1.115 +  {ok: bool}\<close> is the equivalent to \<open>{task: string, ok: bool}\<close>.
   1.116 +
   1.117 +  \<^item> The type expression \<open>t\<^sub>1 | t\<^sub>2\<close> is the disjoint union of two types, either
   1.118 +  one of the two cases may occur.
   1.119 +
   1.120 +
   1.121 +  These types correspond to JSON values in an obvious manner, which is not
   1.122 +  further described here. For example, the JSON array \<^verbatim>\<open>[1, 2, 3]\<close> conforms to
   1.123 +  types \<open>[int]\<close>, \<open>[long]\<close>, \<open>[double]\<close>, \<open>[any]\<close>, \<open>any\<close>.
   1.124 +
   1.125 +  Note that JSON objects require field names to be quoted, but the type
   1.126 +  language omits quotes for clarity. Thus \<^verbatim>\<open>{"a": 42, "b": "xyz"}\<close> conforms to
   1.127 +  the type \<open>{a: int, b: string}\<close>, for example.
   1.128 +
   1.129 +  \<^medskip>
   1.130 +  The absence of an argument or result is represented by type \<^verbatim>\<open>Unit\<close> in
   1.131 +  Isabelle/Scala: it is written as empty text in the message \<open>argument\<close>
   1.132 +  (\secref{sec:input-output-messages}). This is not part of the JSON language.
   1.133 +
   1.134 +  Server replies have name tags like \<^verbatim>\<open>OK\<close>, \<^verbatim>\<open>ERROR\<close>: these are used literally
   1.135 +  together with type specifications to indicate the particular name with the
   1.136 +  type of its argument, e.g.\ \<^verbatim>\<open>OK\<close>~\<open>[string]\<close> for a regular result that is a
   1.137 +  list (JSON array) of strings.
   1.138 +
   1.139 +  \<^bigskip>
   1.140 +  Here are some common type definitions, for use in the subsequent
   1.141 +  specifications of command arguments and results.
   1.142 +
   1.143 +  \<^item> \<^bold>\<open>type\<close>~\<open>position = {line?: int, offset?: int, end_offset?: int, file?:
   1.144 +  string, id?: long}\<close> describes a source position within Isabelle source text.
   1.145 +  Only the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
   1.146 +  Detailed \<open>offset\<close> and \<open>end_offset\<close> positions are counted according to
   1.147 +  Isabelle symbols, see @{ML_type Symbol.symbol} in Isabelle/ML @{cite
   1.148 +  "isabelle-implementation"}. The position \<open>id\<close> belongs to the internal
   1.149 +  representation of command transactions in the Isabelle/PIDE protocol.
   1.150 +
   1.151 +  \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
   1.152 +  the \<open>kind\<close> provides some hint about the role and importance of the message.
   1.153 +  The main message kinds are \<^verbatim>\<open>writeln\<close> (for regular output), \<^verbatim>\<open>warning\<close>, and
   1.154 +  \<^verbatim>\<open>error\<close>. The table \<^verbatim>\<open>Markup.messages\<close> in Isabelle/Scala defines further
   1.155 +  message kinds for more specific applications.
   1.156 +
   1.157 +  \<^item> \<^bold>\<open>type\<close>~\<open>error_message = {kind:\<close>~\<^verbatim>\<open>"error"\<close>\<open>, message: string}\<close> refers to
   1.158 +  error messages in particular. These occur routinely with \<^verbatim>\<open>ERROR\<close> or
   1.159 +  \<^verbatim>\<open>FAILED\<close> replies, but also as initial command syntax errors (which are
   1.160 +  omitted in the command specifications below).
   1.161 +
   1.162 +  \<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
   1.163 +  string, session: string}\<close> reports formal progress in loading theories (e.g.\
   1.164 +  when building a session image). Apart from a regular output message, it also
   1.165 +  reveals the formal theory name (e.g.\ \<^verbatim>\<open>HOL.Nat\<close>) and session name (e.g.\
   1.166 +  \<^verbatim>\<open>HOL\<close>). Note that some rare theory names lack a proper session prefix, e.g.
   1.167 +  theory \<^verbatim>\<open>Main\<close> in session \<^verbatim>\<open>HOL\<close>.
   1.168 +
   1.169 +  \<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
   1.170 +  common Isabelle timing information in seconds, usually with a precision of
   1.171 +  three digits after the point (whole milliseconds).
   1.172 +
   1.173 +  \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
   1.174 +  as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
   1.175 +  \<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/UUID.html\<close>.\<close> Such
   1.176 +  identifiers are created as private random numbers of the server and only
   1.177 +  revealed to the client that creates a certain resource (e.g.\ task or
   1.178 +  session). A client may disclose this information for use in a different
   1.179 +  client connection: e.g.\ this allows to share sessions between multiple
   1.180 +  connections.
   1.181 +
   1.182 +  Client commands need to provide syntactically wellformed UUIDs: this is
   1.183 +  trivial to achieve by using only identifiers that have been produced by the
   1.184 +  server beforehand.
   1.185 +
   1.186 +  \<^item> \<^bold>\<open>type\<close>~\<open>task = {task: uuid}\<close> identifies a newly created asynchronous task
   1.187 +  and thus allows the client to control it by the \<^verbatim>\<open>cancel\<close> command. The same
   1.188 +  task identification is included in messages and the final result produced by
   1.189 +  this task.
   1.190 +\<close>
   1.191 +
   1.192 +
   1.193 +subsection \<open>Command \<^verbatim>\<open>help\<close>\<close>
   1.194 +
   1.195 +text \<open>
   1.196 +  \begin{tabular}{ll}
   1.197 +  regular result: & \<^verbatim>\<open>OK\<close> \<open>[string]\<close> \\
   1.198 +  \end{tabular}
   1.199 +  \<^medskip>
   1.200 +
   1.201 +  The \<^verbatim>\<open>help\<close> command has no argument and returns the list of command names
   1.202 +  known to the server. This is occasionally useful for interactive
   1.203 +  experimentation (see also @{tool client} in \secref{sec:tool-client}).
   1.204 +\<close>
   1.205 +
   1.206 +
   1.207 +subsection \<open>Command \<^verbatim>\<open>echo\<close>\<close>
   1.208 +
   1.209 +text \<open>
   1.210 +  \begin{tabular}{ll}
   1.211 +  argument: & \<open>any\<close> \\
   1.212 +  regular result: & \<^verbatim>\<open>OK\<close> \<open>any\<close> \\
   1.213 +  \end{tabular}
   1.214 +  \<^medskip>
   1.215 +
   1.216 +  The \<^verbatim>\<open>echo\<close> command is the identity function: it returns its argument as
   1.217 +  regular result. This is occasionally useful for testing and interactive
   1.218 +  experimentation (see also @{tool client} in \secref{sec:tool-client}).
   1.219 +
   1.220 +  The type of \<^verbatim>\<open>echo\<close> is actually more general than given above: \<^verbatim>\<open>Unit\<close>,
   1.221 +  \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close> are supported uniformly. Note that \<^verbatim>\<open>XML.Elem\<close> might
   1.222 +  be difficult to type on the console in its YXML syntax
   1.223 +  (\secref{sec:yxml-vs-xml}).
   1.224 +\<close>
   1.225 +
   1.226 +
   1.227 +subsection \<open>Command \<^verbatim>\<open>shutdown\<close>\<close>
   1.228 +
   1.229 +text \<open>
   1.230 +  \begin{tabular}{ll}
   1.231 +  regular result: & \<^verbatim>\<open>OK\<close> \\
   1.232 +  \end{tabular}
   1.233 +  \<^medskip>
   1.234 +
   1.235 +  The \<^verbatim>\<open>shutdown\<close> command has no argument and result value. It forces a
   1.236 +  shutdown of the connected server process, stopping all open sessions and
   1.237 +  closing the server socket. This may disrupt pending commands on other
   1.238 +  connections!
   1.239 +
   1.240 +  \<^medskip>
   1.241 +  Likewise, the command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server
   1.242 +  connection and issues a \<^verbatim>\<open>shutdown\<close> command (see also
   1.243 +  \secref{sec:tool-server}).
   1.244 +\<close>
   1.245 +
   1.246 +
   1.247 +subsection \<open>Command \<^verbatim>\<open>cancel\<close>\<close>
   1.248 +
   1.249 +text \<open>
   1.250 +  \begin{tabular}{ll}
   1.251 +  argument: & \<open>uuid\<close> \\
   1.252 +  regular result: & \<^verbatim>\<open>OK\<close> \\
   1.253 +  \end{tabular}
   1.254 +  \<^medskip>
   1.255 +
   1.256 +  The command invocation \<^verbatim>\<open>cancel "\<close>\<open>id\<close>\<^verbatim>\<open>"\<close> attempts to cancel the specified
   1.257 +  task.
   1.258 +
   1.259 +  Cancellation is merely a hint that the client prefers an ongoing process to
   1.260 +  be stopped. The command always succeeds formally, but it may get ignored by
   1.261 +  a task that is still running, or it might refer to a non-existing or
   1.262 +  no-longer existing task without producing an error.
   1.263 +
   1.264 +  Successful cancellation typically leads to an asynchronous failure of type
   1.265 +  \<^verbatim>\<open>FAILED {\<close>\<open>task: string, message: \<close>\<^verbatim>\<open>"Interrupt"}\<close> --- or a slightly
   1.266 +  different message, depending how the task handles the event.
   1.267 +\<close>
   1.268 +
   1.269 +
   1.270 +subsection \<open>Command \<^verbatim>\<open>session_build\<close> \label{sec:command-session-build}\<close>
   1.271 +
   1.272 +text \<open>
   1.273 +  \begin{tabular}{lll}
   1.274 +  argument: & \<open>session_build_args\<close> \\
   1.275 +  immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   1.276 +  notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
   1.277 +  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_build_results\<close> \\
   1.278 +  error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_build_results\<close> \\[2ex]
   1.279 +  \end{tabular}
   1.280 +
   1.281 +  \begin{tabular}{lll}
   1.282 +  \<^bold>\<open>type\<close> \<open>session_build_args =\<close> \\
   1.283 +  \quad\<open>{session: string,\<close> \\
   1.284 +  \quad~~\<open>preferences?: string,\<close> & \<^bold>\<open>default:\<close> server preferences \\
   1.285 +  \quad~~\<open>options?: [string],\<close> \\
   1.286 +  \quad~~\<open>dirs?: [string],\<close> \\
   1.287 +  \quad~~\<open>ancestor_session?: string,\<close> \\
   1.288 +  \quad~~\<open>all_known?: bool,\<close> \\
   1.289 +  \quad~~\<open>focus_session?: bool,\<close> \\
   1.290 +  \quad~~\<open>required_session?: bool,\<close> \\
   1.291 +  \quad~~\<open>system_mode?: bool,\<close> \\
   1.292 +  \quad~~\<open>verbose?: bool}\<close> \\[2ex]
   1.293 +
   1.294 +  \<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
   1.295 +  \quad\<open>{ok: bool,\<close> \\
   1.296 +  \quad~~\<open>return_code: int,\<close> \\
   1.297 +  \quad~~\<open>sessions: [session_build_result]}\<close> \\[2ex]
   1.298 +
   1.299 +  \<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
   1.300 +  \quad\<open>{session: string,\<close> \\
   1.301 +  \quad~~\<open>ok: bool,\<close> \\
   1.302 +  \quad~~\<open>return_code: int,\<close> \\
   1.303 +  \quad~~\<open>timeout: bool,\<close> \\
   1.304 +  \quad~~\<open>timing: timing}\<close> \\
   1.305 +  \end{tabular}
   1.306 +\<close>
   1.307 +
   1.308 +text \<open>
   1.309 +  The \<^verbatim>\<open>session_build\<close> command prepares given a session image for interactive
   1.310 +  use of theories. This is a limited version of command-line tool @{tool
   1.311 +  build} (\secref{sec:tool-build}), with specific options to request a formal
   1.312 +  context of an interactive session: it also resembles options of @{tool
   1.313 +  jedit} @{cite "isabelle-jedit"}.
   1.314 +
   1.315 +  The build process is asynchronous, with notifications that inform about the
   1.316 +  progress of loaded theories. Some further human-readable messages may be
   1.317 +  output as well.
   1.318 +
   1.319 +  Coordination of independent build processes is at the discretion of the
   1.320 +  client: as for like @{tool build} there are no built-in measures against
   1.321 +  conflicting builds with overlapping hierarchies of session images.
   1.322 +\<close>
   1.323 +
   1.324 +
   1.325 +subsubsection \<open>Arguments\<close>
   1.326 +
   1.327 +text \<open>
   1.328 +  The field \<open>session\<close> is mandatory. It specifies the target session name:
   1.329 +  either directly (default) or indirectly (if \<open>required_session\<close> is
   1.330 +  \<^verbatim>\<open>true\<close>).
   1.331 +
   1.332 +  \<^medskip>
   1.333 +  The environment of Isabelle system options is determined from \<open>preferences\<close>
   1.334 +  that are augmented by \<open>options\<close>, which is a list individual updates of the
   1.335 +  form the \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> (the latter abbreviates
   1.336 +  \<open>name\<close>\<^verbatim>\<open>=true\<close>); see also command-line option \<^verbatim>\<open>-o\<close> for @{tool build}. The
   1.337 +  preferences are loaded from the file
   1.338 +  \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> by default, but the client may
   1.339 +  provide alternative contents for it (as text, not a file-name). This could
   1.340 +  be relevant in situations where client and server run in different
   1.341 +  operating-system contexts.
   1.342 +
   1.343 +  \<^medskip>
   1.344 +  The \<open>dirs\<close> field specifies additional directories for session ROOT files
   1.345 +  (\secref{sec:session-root}). This augments the name space of available
   1.346 +  sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build} or @{tool jedit}.
   1.347 +
   1.348 +  \<^medskip>
   1.349 +  The \<open>ancestor_session\<close> field specifies an alternative image as starting
   1.350 +  point for the target image. The default is to use the parent session
   1.351 +  according to the ROOT entry; see also option \<^verbatim>\<open>-A\<close> in @{tool jedit}. This
   1.352 +  can lead to a more light-weight build process, by skipping intermediate
   1.353 +  session images of the hierarchy that are not used later on.
   1.354 +
   1.355 +  \<^medskip>
   1.356 +  The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all existing sessions from
   1.357 +  reachable ROOT entries in the name space of theories with a proper
   1.358 +  session-qualified name (instead of referring to the file-system location).
   1.359 +  This could be relevant for the \<^verbatim>\<open>use_theories\<close> command
   1.360 +  (\secref{sec:command-use-theories}) to refer to arbitrary theories from
   1.361 +  other sessions. Note that considerable time is required to explore all
   1.362 +  accessible session directories and theory dependencies.
   1.363 +
   1.364 +  \<^medskip>
   1.365 +  The \<open>focus_session\<close> field set to \<^verbatim>\<open>true\<close> to focuses on the target session:
   1.366 +  the accessible name space of theories is restricted to sessions that are
   1.367 +  connected to it.
   1.368 +
   1.369 +  \<^medskip>
   1.370 +  The \<open>required_session\<close> field set to \<^verbatim>\<open>true\<close> indicates that the target image
   1.371 +  should not be the \<open>session\<close>, but its parent (or ancestor according to
   1.372 +  \<open>ancestor_session\<close>). Thus it prepares a session context where theories from
   1.373 +  the \<open>session\<close> itself can be loaded.
   1.374 +
   1.375 +  \<^medskip>
   1.376 +  The \<open>system_mode\<close> field may be set to \<^verbatim>\<open>true\<close> to store session images and
   1.377 +  log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
   1.378 +  @{setting ISABELLE_OUTPUT} (which is normally in @{setting
   1.379 +  ISABELLE_HOME_USER}, i.e.\ the user's home directory). See also option \<^verbatim>\<open>-s\<close>
   1.380 +  in @{tool build} and @{tool jedit}.
   1.381 +
   1.382 +  \<^medskip>
   1.383 +  The \<open>verbose\<close> field may be set to \<^verbatim>\<open>true\<close> for extra verbosity. The effect is
   1.384 +  similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
   1.385 +\<close>
   1.386 +
   1.387 +
   1.388 +subsubsection \<open>Intermediate output\<close>
   1.389 +
   1.390 +text \<open>
   1.391 +  The asynchronous notifications of command \<^verbatim>\<open>session_build\<close> mainly serve as
   1.392 +  progress indicator: the output resembles that of the session build window of
   1.393 +  Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
   1.394 +
   1.395 +  For the client it is usually sufficient to print the messages in plain text,
   1.396 +  but note that \<open>theory_progress\<close> also reveals the internal \<open>theory\<close> and
   1.397 +  \<open>session\<close> names.
   1.398 +\<close>
   1.399 +
   1.400 +
   1.401 +subsubsection \<open>Results\<close>
   1.402 +
   1.403 +text \<open>
   1.404 +  The overall \<open>session_build_results\<close> contain both a summary and and entry
   1.405 +  \<open>session_build_result\<close> for each session in the build hierarchy, leading up
   1.406 +  to the specified target session. The result is always provided,
   1.407 +  independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or failure (\<^verbatim>\<open>FAILED\<close>
   1.408 +  task).
   1.409 +
   1.410 +  The \<open>ok\<close> field tells abstractly, whether all required session builds came
   1.411 +  out as \<open>ok\<close>, i.e.\ \<open>return_code\<close>. A non-zero \<open>return_code\<close> indicates an
   1.412 +  error according to usual POSIX conventions for process exit.
   1.413 +
   1.414 +  For individual \<open>session_build_result\<close> entries, there are additional fields:
   1.415 +  \<open>timeout\<close> to tell if the build process was aborted after running too long,
   1.416 +  and \<open>timing\<close> for the overall process timing in the usual Isabelle format
   1.417 +  with elapsed, CPU, gc time.
   1.418 +\<close>
   1.419 +
   1.420 +
   1.421 +subsubsection \<open>Examples\<close>
   1.422 +
   1.423 +text \<open>
   1.424 +  Build of a session image from the Isabelle distribution:
   1.425 +  @{verbatim [display] \<open>session_build {"session": "HOL-Word"}\<close>}
   1.426 +
   1.427 +  Build a session image from the Archive of Formal Proofs:
   1.428 +  @{verbatim [display] \<open>session_build {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
   1.429 +
   1.430 +  Build of a session image of \<^verbatim>\<open>HOL-Number_Theory\<close> directly on top of \<^verbatim>\<open>HOL\<close>:
   1.431 +  @{verbatim [display] \<open>session_build {"session": "HOL-Number_Theory", "ancestor_session": "HOL"}\<close>}
   1.432 +\<close>
   1.433 +
   1.434 +
   1.435 +subsection \<open>Command \<^verbatim>\<open>session_start\<close> \label{sec:command-session-start}\<close>
   1.436 +
   1.437 +text \<open>
   1.438 +  \begin{tabular}{lll}
   1.439 +  argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\
   1.440 +  immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   1.441 +  notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
   1.442 +  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_start_result\<close> \\
   1.443 +  error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex]
   1.444 +  \end{tabular}
   1.445 +
   1.446 +  \begin{tabular}{l}
   1.447 +  \<^bold>\<open>type\<close> \<open>session_start_result = {session: string, session_id: uuid}\<close>
   1.448 +  \end{tabular}
   1.449 +
   1.450 +  \<^medskip>
   1.451 +  The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with
   1.452 +  underlying Isabelle/ML process, based on a session image that it produces on
   1.453 +  demand in the same manner as \<^verbatim>\<open>session_build\<close>. Thus it accepts all
   1.454 +  \<open>session_build_args\<close> and produces similar notifications, but the detailed
   1.455 +  \<open>session_build_results\<close> are omitted.
   1.456 +
   1.457 +  The session build and startup process is asynchronous: when the task is
   1.458 +  finished, the session remains active for commands such as \<^verbatim>\<open>use_theories\<close>
   1.459 +  (\secref{sec:command-use-theories}), until a \<^verbatim>\<open>session_stop\<close> or \<^verbatim>\<open>shutdown\<close>
   1.460 +  command is sent to the server.
   1.461 +
   1.462 +  Sessions are independent of client connections: it is possible to start a
   1.463 +  session and later apply \<^verbatim>\<open>use_theories\<close> on different connections, as long as
   1.464 +  the internal session identifier is known.
   1.465 +\<close>
   1.466 +
   1.467 +
   1.468 +subsubsection \<open>Arguments\<close>
   1.469 +
   1.470 +text \<open>
   1.471 +  Most of the arguments are the same as for \<^verbatim>\<open>session_build\<close>
   1.472 +  (\secref{sec:command-session-build}).
   1.473 +
   1.474 +  \<^medskip>
   1.475 +  The \<open>print_mode\<close> field adds identifiers of print modes to be made active for
   1.476 +  this session. For example, \<^verbatim>\<open>"print_mode": ["ASCII"]\<close> prefers ASCII
   1.477 +  replacement syntax over mathematical Isabelle symbols. See also option \<^verbatim>\<open>-m\<close>
   1.478 +  in @{tool process} (\secref{sec:tool-process}).
   1.479 +\<close>
   1.480 +
   1.481 +
   1.482 +subsubsection \<open>Results\<close>
   1.483 +
   1.484 +text \<open>
   1.485 +  The \<open>session\<close> field provides the active session name for clarity.
   1.486 +
   1.487 +  \<^medskip>
   1.488 +  The \<open>session_id\<close> field provides the internal identification of the session
   1.489 +  object within the sever process. It can remain active as long as the server
   1.490 +  is running, independently of the current client connection.
   1.491 +\<close>
   1.492 +
   1.493 +
   1.494 +subsection \<open>Examples\<close>
   1.495 +
   1.496 +text \<open>
   1.497 +  Start a default Isabelle/HOL session:
   1.498 +  @{verbatim [display] \<open>session_start {"session": "HOL"}\<close>}
   1.499 +\<close>
   1.500 +
   1.501 +
   1.502 +subsection \<open>Command \<^verbatim>\<open>session_stop\<close>\<close>
   1.503 +
   1.504 +text \<open>
   1.505 +  \begin{tabular}{ll}
   1.506 +  argument: & \<open>{session_id?: uuid}\<close> \\
   1.507 +  immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   1.508 +  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_stop_result\<close> \\
   1.509 +  error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_stop_result\<close> \\[2ex]
   1.510 +  \end{tabular}
   1.511 +
   1.512 +  \begin{tabular}{l}
   1.513 +  \<^bold>\<open>type\<close> \<open>session_stop_result = {ok: bool, return_code: int}\<close>
   1.514 +  \end{tabular}
   1.515 +
   1.516 +  \<^medskip>
   1.517 +  The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified
   1.518 +  Isabelle/PIDE session. This asynchronous tasks usually finishes quickly.
   1.519 +  Failure only happens unusual situations, according to the return code of the
   1.520 +  underlying Isabelle/ML process.
   1.521 +\<close>
   1.522 +
   1.523 +
   1.524 +subsubsection \<open>Arguments\<close>
   1.525 +
   1.526 +text \<open>
   1.527 +  The \<open>session_id\<close> field is the UUID originally created by the server for the
   1.528 +  intended session.
   1.529 +\<close>
   1.530 +
   1.531 +
   1.532 +subsubsection \<open>Results\<close>
   1.533 +
   1.534 +text \<open>
   1.535 +  The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process terminated
   1.536 +  properly. The \<open>return_code\<close> expresses this information according to usual
   1.537 +  POSIX conventions for process exit.
   1.538 +\<close>
   1.539 +
   1.540 +
   1.541 +subsection \<open>Command \<^verbatim>\<open>use_theories\<close> \label{sec:command-use-theories}\<close>
   1.542 +
   1.543 +text \<open>
   1.544 +  \begin{tabular}{ll}
   1.545 +  argument: & \<open>use_theories_arguments\<close> \\
   1.546 +  regular result: & \<^verbatim>\<open>OK\<close> \<open>use_theories_results\<close> \\
   1.547 +  \end{tabular}
   1.548 +
   1.549 +  \begin{tabular}{ll}
   1.550 +  \<^bold>\<open>type\<close> \<open>theory_name = string | {name: string, pos: position}\<close> \\
   1.551 +  \end{tabular}
   1.552 +
   1.553 +  \begin{tabular}{ll}
   1.554 +  \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
   1.555 +  \quad\<open>{session_id: uuid,\<close> \\
   1.556 +  \quad~~\<open>theories: [theory_name],\<close> \\
   1.557 +  \quad~~\<open>qualifier?: string,\<close> \\
   1.558 +  \quad~~\<open>master_dir?: string,\<close> \\
   1.559 +  \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   1.560 +  \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
   1.561 +
   1.562 +  \<^bold>\<open>type\<close> \<open>node_status =\<close> \\
   1.563 +  \quad\<open>{ok: bool,\<close> \\
   1.564 +  \quad~~\<open>total: int,\<close> \\
   1.565 +  \quad~~\<open>unprocessed: int,\<close> \\
   1.566 +  \quad~~\<open>running: int,\<close> \\
   1.567 +  \quad~~\<open>warned: int,\<close> \\
   1.568 +  \quad~~\<open>failed: int,\<close> \\
   1.569 +  \quad~~\<open>finished: int,\<close> \\
   1.570 +  \quad~~\<open>consolidated: bool}\<close> \\[2ex]
   1.571 +
   1.572 +  \<^bold>\<open>type\<close> \<open>node_result =\<close> \\
   1.573 +  \quad\<open>{node_name: string,\<close> \\
   1.574 +  \quad~~\<open>theory: string,\<close> \\
   1.575 +  \quad~~\<open>status: node_status,\<close> \\
   1.576 +  \quad~~\<open>messages: [message]}\<close> \\[2ex]
   1.577 +
   1.578 +  \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
   1.579 +  \quad\<open>{ok: bool,\<close> \\
   1.580 +  \quad~~\<open>errors: [message],\<close> \\
   1.581 +  \quad~~\<open>nodes: [node_result]}\<close> \\[2ex]
   1.582 +  \end{tabular}
   1.583 +
   1.584 +  \<^medskip>
   1.585 +
   1.586 +  The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
   1.587 +  current version of given theory files to it: theory dependencies are
   1.588 +  resolved implicitly. The command succeeds eventually, when all theories have
   1.589 +  been \<^emph>\<open>consolidated\<close> in the sense that the outermost command structure has
   1.590 +  finished (or failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been
   1.591 +  checked.
   1.592 +\<close>
   1.593 +
   1.594 +
   1.595 +subsubsection \<open>Arguments\<close>
   1.596 +
   1.597 +text \<open>
   1.598 +  The \<open>session_id\<close> is the identifier provided by the server, when the session
   1.599 +  was created (possibly on a different client connection).
   1.600 +
   1.601 +  \<^medskip>
   1.602 +  The \<open>theories\<close> field specifies theory names as in \<^theory_text>\<open>theory imports\<close> or in
   1.603 +  session ROOT \<^verbatim>\<open>theories\<close>: an explicit source position for these theory name
   1.604 +  specifications may be given as well, which is occasionally useful for
   1.605 +  precise error locations.
   1.606 +
   1.607 +  \<^medskip>
   1.608 +  The \<open>qualifier\<close> field provides an alternative session qualifier for theories
   1.609 +  that are not formally recognized as a member of a particular session. The
   1.610 +  default is \<^verbatim>\<open>Draft\<close> as in Isabelle/jEdit. There is rarely a need to change
   1.611 +  that, as theory nodes are already uniquely identified by their physical
   1.612 +  file-system location.
   1.613 +
   1.614 +  \<^medskip>
   1.615 +  The \<open>master_dir\<close> field explicit specifies the formal master directory of the
   1.616 +  imported theory. Normally this is determined implicitly from the parent
   1.617 +  directory of the physical theory file location.
   1.618 +
   1.619 +  \<^medskip>
   1.620 +  The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
   1.621 +  default is for classic console output. Formatting happens at the end of
   1.622 +  \<^verbatim>\<open>use_theories\<close>, when all prover messages produced are exported to the
   1.623 +  client.
   1.624 +
   1.625 +  \<^medskip>
   1.626 +  The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> means that message output is
   1.627 +  rendered for direct output on a Unicode capable channel, ideally with the
   1.628 +  Isabelle fonts as in Isabelle/jEdit (or Isabelle HTML output). The default
   1.629 +  is to keep the symbolic representation of Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead
   1.630 +  of its rendering as \<open>\<forall>\<close>. This means the client needs to perform its own
   1.631 +  rendering to present it to the end-user.
   1.632 +\<close>
   1.633 +
   1.634 +subsubsection \<open>Results\<close>
   1.635 +
   1.636 +text \<open>
   1.637 +  The \<open>ok\<close> field indicates overall success of processing the specified
   1.638 +  theories with all their dependencies.
   1.639 +
   1.640 +  When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively,
   1.641 +  including position information for the theory nodes where the error happened
   1.642 +  (this includes imported theories).
   1.643 +
   1.644 +  \<^medskip>
   1.645 +  The \<open>nodes\<close> field provides more detailed information about each imported
   1.646 +  theory node. Here the individual fields are as follows:
   1.647 +
   1.648 +  \<^item> \<open>node_name\<close>: the physical name for the theory node, based on its
   1.649 +  file-system location;\<^footnote>\<open>Clients may recognize the originally provided
   1.650 +  file-names after careful normalization in the file-system of the server.\<close>
   1.651 +
   1.652 +  \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close> or
   1.653 +  \<^verbatim>\<open>Draft.Test\<close>;
   1.654 +
   1.655 +  \<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
   1.656 +  \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
   1.657 +
   1.658 +  \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory note
   1.659 +  (\<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>, etc.).
   1.660 +\<close>
   1.661 +
   1.662 +
   1.663 +subsubsection \<open>Examples\<close>
   1.664 +
   1.665 +text \<open>
   1.666 +  Process some example theory from the Isabelle distribution, within the
   1.667 +  context of an already started session for Isabelle/HOL (see also
   1.668 +  \secref{sec:command-session-start}):
   1.669 +  @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Isar_Examples/Drinker"]}\<close>}
   1.670 +
   1.671 +  \<^medskip>
   1.672 +  Process some example theories that import other theories via
   1.673 +  session-qualified theory names:
   1.674 +
   1.675 +  @{verbatim [display] \<open>session_start {"session": "HOL", "all_known": true}
   1.676 +use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
   1.677 +session_stop {"session_id": ...}\<close>}
   1.678 +
   1.679 +  The option \<open>all_known\<close> has been used here to the full name space of
   1.680 +  session-qualified theory names accessible in this session. This is also the
   1.681 +  default in Isabelle/jEdit, although it requires significant startup time.
   1.682 +
   1.683 +  \<^medskip>
   1.684 +  Process some example theories in the context of their (single) parent
   1.685 +  session:
   1.686 +
   1.687 +  @{verbatim [display] \<open>session_start {"session": "HOL-Library"}
   1.688 +use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
   1.689 +session_stop {"session_id": ...}\<close>}
   1.690  \<close>
   1.691  
   1.692  end