author wenzelm
Thu Mar 22 14:27:32 2018 +0100 (15 months ago)
changeset 67918 7dc204623770
parent 67917 d13b2dd20f5e
child 67919 dd90faed43b2
permissions -rw-r--r--
misc tuning and clarification;
     1 (*:maxLineLen=78:*)
     3 theory Server
     4 imports Base
     5 begin
     7 chapter \<open>The Isabelle server\<close>
     9 text \<open>
    10   An Isabelle session requires at least two processes, which are both rather
    11   heavy: Isabelle/Scala for the system infrastructure and Isabelle/ML for the
    12   logic session (e.g.\ HOL). In principle, these processes can be invoked
    13   directly on the command-line, e.g.\ via @{tool java}, @{tool scala}, @{tool
    14   process}, @{tool console}, but this approach is inadequate for reactive
    15   applications that require quick responses from the prover.
    17   In contrast, the Isabelle server exposes Isabelle/Scala as a
    18   ``terminate-stay-resident'' application that manages multiple logic
    19   \<^emph>\<open>sessions\<close> and concurrent tasks to use \<^emph>\<open>theories\<close>. This provides an
    20   analogous to @{ML Thy_Info.use_theories} in Isabelle/ML, but with full
    21   concurrency and Isabelle/PIDE markup.
    23   The client/server arrangement via TCP sockets also opens possibilities for
    24   remote Isabelle services that are accessed by local applications, e.g.\ via
    25   an SSH tunnel.
    26 \<close>
    29 section \<open>Command-line tools\<close>
    31 subsection \<open>Server \label{sec:tool-server}\<close>
    33 text \<open>
    34   The @{tool_def server} tool manages resident server processes:
    35   @{verbatim [display]
    36 \<open>Usage: isabelle server [OPTIONS]
    38   Options are:
    39     -L FILE      logging on FILE
    40     -c           console interaction with specified server
    41     -l           list servers (alternative operation)
    42     -n NAME      explicit server name (default: isabelle)
    43     -p PORT      explicit server port
    44     -s           assume existing server, no implicit startup
    45     -x           exit specified server (alternative operation)
    47   Manage resident Isabelle servers.\<close>}
    49   The main operation of \<^verbatim>\<open>isabelle server\<close> is to ensure that a named server is
    50   running, either by finding an already running process (according to the
    51   central database file @{path "$ISABELLE_HOME_USER/servers.db"}) or by
    52   becoming itself a new server that accepts connections on a particular TCP
    53   socket. The server name and its address are printed as initial output line.
    54   If another server instance is already running, the current
    55   \<^verbatim>\<open>isabelle server\<close> process will terminate; otherwise, it keeps running as a
    56   new server process until an explicit \<^verbatim>\<open>shutdown\<close> command is received.
    57   Further details of the server socket protocol are explained in
    58   \secref{sec:server-protocol}.
    60   Other server management operations are invoked via options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-x\<close>
    61   (see below).
    63   \<^medskip>
    64   Option \<^verbatim>\<open>-n\<close> specifies an alternative server name: at most one process for
    65   each name may run, but each server instance supports multiple connections
    66   and logic sessions.
    68   \<^medskip>
    69   Option \<^verbatim>\<open>-p\<close> specifies an explicit TCP port for the server socket (which is
    70   always on \<^verbatim>\<open>localhost\<close>): the default is to let the operating system assign a
    71   free port number.
    73   \<^medskip>
    74   Option \<^verbatim>\<open>-s\<close> strictly assumes that the specified server process is already
    75   running, skipping the optional server startup phase.
    77   \<^medskip>
    78   Option \<^verbatim>\<open>-c\<close> connects the console in/out channels after the initial check
    79   for a suitable server process. Also note that the @{tool client} tool
    80   (\secref{sec:tool-client}) provides a command-line editor to interact with
    81   the server.
    83   \<^medskip>
    84   Option \<^verbatim>\<open>-L\<close> specifies a log file for exceptional output of internal server
    85   and session operations.
    87   \<^medskip>
    88   Operation \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
    89   details.
    91   \<^medskip>
    92   Operation \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a
    93   \<^verbatim>\<open>shutdown\<close> command.
    94 \<close>
    97 subsection \<open>Client \label{sec:tool-client}\<close>
    99 text \<open>
   100   The @{tool_def client} tool provides console interaction for Isabelle
   101   servers:
   102   @{verbatim [display]
   103 \<open>Usage: isabelle client [OPTIONS]
   105   Options are:
   106     -n NAME      explicit server name
   107     -p PORT      explicit server port
   109   Console interaction for Isabelle server (with line-editor).\<close>}
   111   This is a wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
   112   experimentation, which uses @{setting ISABELLE_LINE_EDITOR} if available.
   113   The server name is sufficient for identification, as the client can
   114   determine the connection details from the local database of active servers.
   116   \<^medskip>
   117   Option \<^verbatim>\<open>-n\<close> specifies an explicit server name as in @{tool server}.
   119   \<^medskip>
   120   Option \<^verbatim>\<open>-p\<close> specifies an explicit server port as in @{tool server}.
   121 \<close>
   124 subsection \<open>Examples\<close>
   126 text \<open>
   127   Ensure that a particular server instance is running in the background:
   128   @{verbatim [display] \<open>isabelle server -n test &\<close>}
   130   The first line of output presents the connection details:\<^footnote>\<open>This information
   131   may be used in other TCP clients, without access to Isabelle/Scala and the
   132   underlying database of running servers.\<close>
   133   @{verbatim [display] \<open>server "test" = (password "XYZ")\<close>}
   135   \<^medskip>
   136   List available server processes:
   137   @{verbatim [display] \<open>isabelle server -l\<close>}
   139   \<^medskip>
   140   Connect the command-line client to the above test server:
   141   @{verbatim [display] \<open>isabelle client -n test\<close>}
   143   Interaction now works on a line-by-line basis, with commands like \<^verbatim>\<open>help\<close> or
   144   \<^verbatim>\<open>echo\<close>. For example, some JSON values may be echoed like this:
   146   @{verbatim [display]
   147 \<open>echo 42
   148 echo [1, 2, 3]
   149 echo {"a": "text", "b": true, "c": 42}\<close>}
   151   Closing the connection (via CTRL-D) leaves the server running: it is
   152   possible to reconnect again, and have multiple connections at the same time.
   154   \<^medskip>
   155   Exit the named server on the command-line:
   156   @{verbatim [display] \<open>isabelle server -n test -x\<close>}
   157 \<close>
   160 section \<open>Protocol messages \label{sec:server-protocol}\<close>
   162 text \<open>
   163   The Isabelle server listens on a regular TCP socket, using a line-oriented
   164   protocol of structured messages. Input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
   165   (via \<^verbatim>\<open>OK\<close> or \<^verbatim>\<open>ERROR\<close>) are strictly alternating on the toplevel, but
   166   commands may also return a \<^emph>\<open>task\<close> identifier to indicate an ongoing
   167   asynchronous process that is joined later (via \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>).
   168   Asynchronous \<^verbatim>\<open>NOTE\<close> messages may occur at any time: they are independent of
   169   the main command-result protocol.
   171   For example, the synchronous \<^verbatim>\<open>echo\<close> command immediately returns its
   172   argument as \<^verbatim>\<open>OK\<close> result. In contrast, the asynchronous \<^verbatim>\<open>session_build\<close>
   173   command returns \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> and continues in the background. It
   174   will eventually produce \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> or
   175   \<^verbatim>\<open>FAILED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> with the final result. Intermediately, it
   176   may emit asynchronous messages of the form \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>
   177   to inform about its progress. Due to the explicit task identifier, the
   178   client can show these messages in the proper context, e.g.\ a GUI window for
   179   this particular session build job.
   181   \medskip Subsequently, the protocol message formats are described in further
   182   detail.
   183 \<close>
   186 subsection \<open>Byte messages\<close>
   188 text \<open>
   189   The client-server connection is a raw byte-channel for bidirectional
   190   communication, but the Isabelle server always works with messages of a
   191   particular length. Messages are written as a single chunk that is flushed
   192   immediately.
   194   Message boundaries are determined as follows:
   196     \<^item> A \<^emph>\<open>short message\<close> consists of a single line: it is a sequence of
   197     arbitrary bytes excluding CR (13) and LF (10), and terminated by CR-LF or
   198     just LF.
   200     \<^item> A \<^emph>\<open>long message\<close> starts with a single that consists only of decimal
   201     digits: these are interpreted as length of the subsequent block of
   202     arbitrary bytes. A final line-terminator (as above) may be included here,
   203     but is not required.
   205   Messages in JSON format (see below) always fit on a single line, due to
   206   escaping of newline characters within string literals. This is convenient
   207   for interactive experimentation, but it can impact performance for very long
   208   messages. If the message byte-length is given on the preceding line, the
   209   server can read the message more efficiently as a single block.
   210 \<close>
   213 subsection \<open>Text messages\<close>
   215 text \<open>
   216   Messages are read and written as byte streams (with byte lengths), but the
   217   content is always interpreted as plain text in terms of the UTF-8
   218   encoding.\<^footnote>\<open>See also the ``UTF-8 Everywhere Manifesto''
   219   \<^url>\<open>\<close>.\<close>
   221   Note that line-endings and other formatting characters are invariant wrt.
   222   UTF-8 representation of text: thus implementations are free to determine the
   223   overall message structure before or after applying the text encoding.
   224 \<close>
   227 subsection \<open>Input and output messages \label{sec:input-output-messages}\<close>
   229 text \<open>
   230   Server input and output messages have a uniform format as follows:
   232     \<^item> \<open>name argument\<close> such that:
   234     \<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
   235     ``\<^verbatim>\<open>_\<close>'', ``\<^verbatim>\<open>.\<close>'',
   237     \<^item> the separator between \<open>name\<close> and \<open>argument\<close> is the longest possible
   238     sequence of ASCII blanks (it could be empty, e.g.\ when the argument
   239     starts with a quote or bracket),
   241     \<^item> \<open>argument\<close> is the rest of the message without line terminator.
   243   \<^medskip>
   244   Input messages are sent from the client to the server. Here the \<open>name\<close>
   245   specifies a \<^emph>\<open>server command\<close>: the list of known commands may be
   246   retrieved via the \<^verbatim>\<open>help\<close> command.
   248   \<^medskip>
   249   Output messages are sent from the server to the client. Here the \<open>name\<close>
   250   specifies the \<^emph>\<open>server reply\<close>, which always has a specific meaning as
   251   follows:
   253     \<^item> synchronous results: \<^verbatim>\<open>OK\<close> or \<^verbatim>\<open>ERROR\<close>
   254     \<^item> asynchronous results: \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>
   255     \<^item> intermediate notifications: \<^verbatim>\<open>NOTE\<close>
   257   \<^medskip>
   258   The \<open>argument\<close> format is uniform for both input and output messages:
   260     \<^item> empty argument (Scala type \<^verbatim>\<open>Unit\<close>)
   261     \<^item> XML element in YXML notation (Scala type \<^verbatim>\<open>XML.Elem\<close>)
   262     \<^item> JSON value (Scala type \<^verbatim>\<open>JSON.T\<close>)
   264   JSON values may consist of objects (records), arrays (lists), strings,
   265   numbers, bools, null.\<^footnote>\<open>See also the official specification
   266   \<^url>\<open>\<close> and unofficial explorations ``Parsing JSON is a
   267   Minefield'' \<^url>\<open>\<close>.\<close> Since JSON requires
   268   explicit quotes and backslash-escapes to represent arbitrary text, the YXML
   269   notation for XML trees (\secref{sec:yxml-vs-xml}) works better
   270   for large messages with a lot of PIDE markup.
   272   Nonetheless, the most common commands use JSON by default: big chunks of
   273   text (theory sources etc.) are taken from the underlying file-system and
   274   results are pre-formatted for plain-text output, without PIDE markup
   275   information. This is a concession to simplicity: the server imitates the
   276   appearance of command-line tools on top of the Isabelle/PIDE infrastructure.
   277 \<close>
   280 subsection \<open>Initial password exchange\<close>
   282 text \<open>
   283   Whenever a new client opens the server socket, the initial message needs to
   284   be its unique password. The server replies either with \<^verbatim>\<open>OK\<close> (and some
   285   information about the Isabelle version) or by silent disconnection of what
   286   is considered an illegal connection attempt. Note that @{tool client}
   287   already presents the correct password internally.
   289   Server passwords are created as Universally Unique Identifier (UUID) in
   290   Isabelle/Scala and stored in a per-user database, with restricted
   291   file-system access only for the current user. The Isabelle/Scala server
   292   implementation is careful to expose the password only on private output
   293   channels, and not on a process command-line (which is accessible to other
   294   users, e.g.\ via the \<^verbatim>\<open>ps\<close> command).
   295 \<close>
   298 subsection \<open>Synchronous commands\<close>
   300 text \<open>
   301   A \<^emph>\<open>synchronous command\<close> corresponds to regular function application in
   302   Isabelle/Scala, with single argument and result (regular or error). Both the
   303   argument and the result may consist of type \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close>.
   304   An error result typically consists of a JSON object with error message and
   305   potentially further result fields (this resembles exceptions in Scala).
   307   These are the protocol exchanges for both cases of command execution:
   308   \begin{center}
   309   \begin{tabular}{rl}
   310   \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   311   (a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK\<close> \<open>result\<close> \\
   312   (b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>ERROR\<close> \<open>result\<close> \\
   313   \end{tabular}
   314   \end{center}
   315 \<close>
   318 subsection \<open>Asynchronous commands\<close>
   320 text \<open>
   321   An \<^emph>\<open>asynchronous command\<close> corresponds to an ongoing process that finishes
   322   or fails eventually, while emitting arbitrary notifications in between.
   323   Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close>
   324   giving the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad
   325   command syntax. For a running task, the termination is indicated later by
   326   \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result value.
   328   These are the protocol exchanges for various cases of command task
   329   execution:
   331   \begin{center}
   332   \begin{tabular}{rl}
   333   \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   334   immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> \\
   335   intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   336   (a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   337   (b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FAILED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\[3ex]
   338   \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   339   immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>ERROR\<close>~\<open>\<dots>\<close> \\
   340   \end{tabular}
   341   \end{center}
   343   All asynchronous messages are decorated with the task identifier that was
   344   revealed in the immediate (synchronous) result. Thus the client can
   345   invoke further asynchronous commands and still dispatch the resulting stream of
   346   asynchronous messages properly.
   348   The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
   349   prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is not guaranteed:
   350   the cancel event may come too late or the running process may just ignore
   351   it.
   352 \<close>
   355 section \<open>Types for JSON values \label{sec:json-types}\<close>
   357 text \<open>
   358   In order to specify concrete JSON types for command arguments and result
   359   messages, the following type definition language shall be used:
   361   \<^rail>\<open>
   362     @{syntax type_def}: @'type' @{syntax name} '=' @{syntax type}
   363     ;
   364     @{syntax type}: @{syntax name} | @{syntax value} | 'any' | 'null' |
   365       'bool' | 'int' | 'long' | 'double' | 'string' | '[' @{syntax type} ']' |
   366       '{' (@{syntax field_type} ',' *) '}' |
   367       @{syntax type} '\<oplus>' @{syntax type} |
   368       @{syntax type} '|' @{syntax type} |
   369       '(' @{syntax type} ')'
   370     ;
   371     @{syntax field_type}: @{syntax name} ('?'?) ':' @{syntax type}
   372   \<close>
   374   This is a simplified variation of TypeScript
   375   interfaces.\<^footnote>\<open>\<^url>\<open>\<close>\<close>
   376   The meaning of these types is specified wrt. the Isabelle/Scala
   377   implementation as follows.
   379   \<^item> A \<open>name\<close> refers to a type defined elsewhere. The environment of type
   380   definitions is given informally: put into proper foundational order, it
   381   needs to specify a strongly normalizing system of syntactic abbreviations;
   382   type definitions may not be recursive.
   384   \<^item> A \<open>value\<close> in JSON notation represents the singleton type of the given
   385   item. For example, the string \<^verbatim>\<open>"error"\<close> can be used as type for a slot that
   386   is guaranteed to contain that constant.
   388   \<^item> Type \<open>any\<close> is the super type of all other types: it is an untyped slot in
   389   the specification and corresponds to \<^verbatim>\<open>Any\<close> or \<^verbatim>\<open>JSON.T\<close> in Isabelle/Scala.
   391   \<^item> Type \<open>null\<close> is the type of the improper value \<open>null\<close>; it corresponds to
   392   type \<^verbatim>\<open>Null\<close> in Scala and is normally not used in Isabelle/Scala.\<^footnote>\<open>See also
   393   ``Null References: The Billion Dollar Mistake'' by Tony Hoare
   394   \<^url>\<open>\<close>.\<close>
   396   \<^item> Type \<open>bool\<close> is the type of the truth values \<^verbatim>\<open>true\<close> and \<^verbatim>\<open>false\<close>; it
   397   corresponds to \<^verbatim>\<open>Boolean\<close> in Scala.
   399   \<^item> Types \<open>int\<close>, \<open>long\<close>, \<open>double\<close> are specific versions of the generic
   400   \<open>number\<close> type, corresponding to \<^verbatim>\<open>Int\<close>, \<^verbatim>\<open>Long\<close>, \<^verbatim>\<open>Double\<close> in Scala, but
   401   \<^verbatim>\<open>Long\<close> is limited to 53 bit precision.\<^footnote>\<open>Implementations of JSON typically
   402   standardize \<open>number\<close> to \<^verbatim>\<open>Double\<close>, which can absorb \<^verbatim>\<open>Int\<close> faithfully, but
   403   not all of \<^verbatim>\<open>Long\<close>.\<close>
   405   \<^item> Type \<open>string\<close> represents Unicode text; it corresponds to type \<^verbatim>\<open>String\<close> in
   406   Scala.
   408   \<^item> Type \<open>[t]\<close> is the array (or list) type over \<open>t\<close>; it corresponds to
   409   \<^verbatim>\<open>List[t]\<close> in Scala. The list type is co-variant as usual (i.e.\ monotonic
   410   wrt. the subtype relation).
   412   \<^item> Object types describe the possible content of JSON records, with field
   413   names and types. A question mark after a field name means that it is
   414   optional. In Scala this could refer to an explicit type \<^verbatim>\<open>Option[t]\<close>, e.g.\
   415   \<open>{a: int, b?: string}\<close> corresponding to a Scala case class with arguments
   416   \<^verbatim>\<open>a: Int\<close>, \<^verbatim>\<open>b: Option[String]\<close>.
   418   Alternatively, optional fields can have a default value. If nothing else is
   419   specified, a standard ``empty value'' is used for each type, i.e.\ \<^verbatim>\<open>0\<close> for
   420   the number types, \<^verbatim>\<open>false\<close> for \<open>bool\<close>, or the empty string, array, object
   421   etc.
   423   Object types are \<^emph>\<open>permissive\<close> in the sense that only the specified field
   424   names need to conform to the given types, but unspecified fields may be
   425   present as well.
   427   \<^item> The type expression \<open>t\<^sub>1 \<oplus> t\<^sub>2\<close> only works for two object types with
   428   disjoint field names: it is the concatenation of the respective @{syntax
   429   field_type} specifications taken together. For example: \<open>{task: string} \<oplus>
   430   {ok: bool}\<close> is the equivalent to \<open>{task: string, ok: bool}\<close>.
   432   \<^item> The type expression \<open>t\<^sub>1 | t\<^sub>2\<close> is the disjoint union of two types, either
   433   one of the two cases may occur.
   435   \<^item> Parentheses \<open>(t)\<close> merely group type expressions syntactically.
   438   These types correspond to JSON values in an obvious manner, which is not
   439   further described here. For example, the JSON array \<^verbatim>\<open>[1, 2, 3]\<close> conforms to
   440   types \<open>[int]\<close>, \<open>[long]\<close>, \<open>[double]\<close>, \<open>[any]\<close>, \<open>any\<close>.
   442   Note that JSON objects require field names to be quoted, but the type
   443   language omits quotes for clarity. Thus the object \<^verbatim>\<open>{"a": 42, "b": "xyz"}\<close>
   444   conforms to the type \<open>{a: int, b: string}\<close>, for example.
   446   \<^medskip>
   447   The absence of an argument or result is represented by the Scala type
   448   \<^verbatim>\<open>Unit\<close>: it is written as empty text in the message \<open>argument\<close>
   449   (\secref{sec:input-output-messages}). This is not part of the JSON language.
   451   Server replies have name tags like \<^verbatim>\<open>OK\<close>, \<^verbatim>\<open>ERROR\<close>: these are used literally
   452   together with type specifications to indicate the particular name with the
   453   type of its argument, e.g.\ \<^verbatim>\<open>OK\<close>~\<open>[string]\<close> for a regular result that is a
   454   list (JSON array) of strings.
   456   \<^bigskip>
   457   Here are some common type definitions, for use in particular specifications
   458   of command arguments and results.
   460   \<^item> \<^bold>\<open>type\<close>~\<open>position = {line?: int, offset?: int, end_offset?: int, file?:
   461   string, id?: long}\<close> describes a source position within Isabelle text. Only
   462   the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
   463   Detailed \<open>offset\<close> and \<open>end_offset\<close> positions are counted according to
   464   Isabelle symbols, see @{ML_type Symbol.symbol} in Isabelle/ML @{cite
   465   "isabelle-implementation"}. The position \<open>id\<close> belongs to the representation
   466   of command transactions in the Isabelle/PIDE protocol: it normally does not
   467   occur in externalized positions.
   469   \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
   470   the \<open>kind\<close> provides some hint about the role and importance of the message.
   471   The main message kinds are \<^verbatim>\<open>writeln\<close> (for regular output), \<^verbatim>\<open>warning\<close>, and
   472   \<^verbatim>\<open>error\<close>. The table \<^verbatim>\<open>Markup.messages\<close> in Isabelle/Scala defines further
   473   message kinds for more specific applications.
   475   \<^item> \<^bold>\<open>type\<close>~\<open>error_message = {kind:\<close>~\<^verbatim>\<open>"error"\<close>\<open>, message: string}\<close> refers to
   476   error messages in particular. These occur routinely with \<^verbatim>\<open>ERROR\<close> or
   477   \<^verbatim>\<open>FAILED\<close> replies, but also as initial command syntax errors (which are
   478   omitted in the command specifications below).
   480   \<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
   481   string, session: string}\<close> reports formal progress in loading theories (e.g.\
   482   when building a session image). Apart from a regular output message, it also
   483   reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
   484   \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
   485   e.g. theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
   487   \<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
   488   common Isabelle timing information in seconds, usually with a precision of
   489   three digits after the point (whole milliseconds).
   491   \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
   492   as plain text.\<^footnote>\<open>See \<^url>\<open>\<close> and
   493   \<^url>\<open>\<close>.\<close> Such
   494   identifiers are created as private random numbers of the server and only
   495   revealed to the client that creates a certain resource (e.g.\ task or
   496   session). A client may disclose this information for use in a different
   497   client connection: this allows to share sessions between multiple
   498   connections.
   500   Client commands need to provide syntactically wellformed UUIDs: this is
   501   trivial to achieve by using only identifiers that have been produced by the
   502   server beforehand.
   504   \<^item> \<^bold>\<open>type\<close>~\<open>task = {task: uuid}\<close> identifies a newly created asynchronous task
   505   and thus allows the client to control it by the \<^verbatim>\<open>cancel\<close> command. The same
   506   task identification is included in all messages produced by this task.
   508   \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
   509   int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
   510   represents a formal theory node status of the PIDE document model. Fields
   511   \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close> account
   512   for individual commands within a theory node; \<open>ok\<close> is an abstraction for
   513   \<open>failed = 0\<close>. The \<open>consolidated\<close> flag indicates whether the outermost theory
   514   command structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has
   515   been checked.
   516 \<close>
   519 section \<open>Server commands and results\<close>
   521 text \<open>
   522   Here follows an overview of particular Isabelle server commands with their
   523   results, which are usually represented as JSON values with types according
   524   to \secref{sec:json-types}. The general format of input and output messages
   525   is described in \secref{sec:input-output-messages}. The relevant
   526   Isabelle/Scala source files are:
   528   \<^medskip>
   529   \begin{tabular}{l}
   530   \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
   531   \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close> \\
   532   \<^file>\<open>$ISABELLE_HOME/src/Pure/General/json.scala\<close> \\
   533   \end{tabular}
   534 \<close>
   537 subsection \<open>Command \<^verbatim>\<open>help\<close>\<close>
   539 text \<open>
   540   \begin{tabular}{ll}
   541   regular result: & \<^verbatim>\<open>OK\<close> \<open>[string]\<close> \\
   542   \end{tabular}
   543   \<^medskip>
   545   The \<^verbatim>\<open>help\<close> command has no argument and returns the list of server command
   546   names. This is occasionally useful for interactive experimentation (see also
   547   @{tool client} in \secref{sec:tool-client}).
   548 \<close>
   551 subsection \<open>Command \<^verbatim>\<open>echo\<close>\<close>
   553 text \<open>
   554   \begin{tabular}{ll}
   555   argument: & \<open>any\<close> \\
   556   regular result: & \<^verbatim>\<open>OK\<close> \<open>any\<close> \\
   557   \end{tabular}
   558   \<^medskip>
   560   The \<^verbatim>\<open>echo\<close> command is the identity function: it returns its argument as
   561   regular result. This is occasionally useful for testing and interactive
   562   experimentation (see also @{tool client} in \secref{sec:tool-client}).
   564   The Scala type of \<^verbatim>\<open>echo\<close> is actually more general than given above:
   565   \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close> work uniformly. Note that \<^verbatim>\<open>XML.Elem\<close> might
   566   be difficult to type on the console in its YXML syntax
   567   (\secref{sec:yxml-vs-xml}).
   568 \<close>
   571 subsection \<open>Command \<^verbatim>\<open>shutdown\<close>\<close>
   573 text \<open>
   574   \begin{tabular}{ll}
   575   regular result: & \<^verbatim>\<open>OK\<close> \\
   576   \end{tabular}
   577   \<^medskip>
   579   The \<^verbatim>\<open>shutdown\<close> command has no argument and result value. It forces a
   580   shutdown of the connected server process, stopping all open sessions and
   581   closing the server socket. This may disrupt pending commands on other
   582   connections!
   584   \<^medskip>
   585   The command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server connection
   586   and issues a \<^verbatim>\<open>shutdown\<close> command (see also \secref{sec:tool-server}).
   587 \<close>
   590 subsection \<open>Command \<^verbatim>\<open>cancel\<close>\<close>
   592 text \<open>
   593   \begin{tabular}{ll}
   594   argument: & \<open>uuid\<close> \\
   595   regular result: & \<^verbatim>\<open>OK\<close> \\
   596   \end{tabular}
   597   \<^medskip>
   599   The command invocation \<^verbatim>\<open>cancel "\<close>\<open>uuid\<close>\<^verbatim>\<open>"\<close> attempts to cancel the
   600   specified task.
   602   Cancellation is merely a hint that the client prefers an ongoing process to
   603   be stopped. The command always succeeds formally, but it may get ignored by
   604   a task that is still running; it might also refer to a non-existing or
   605   no-longer existing task (without producing an error).
   607   Successful cancellation typically leads to an asynchronous failure of type
   608   \<^verbatim>\<open>FAILED {\<close>\<open>task: uuid, message:\<close>~\<^verbatim>\<open>"Interrupt"}\<close>. A different message is
   609   also possible, depending how the task handles the event.
   610 \<close>
   613 subsection \<open>Command \<^verbatim>\<open>session_build\<close> \label{sec:command-session-build}\<close>
   615 text \<open>
   616   \begin{tabular}{lll}
   617   argument: & \<open>session_build_args\<close> \\
   618   immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   619   notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
   620   regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_build_results\<close> \\
   621   error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_build_results\<close> \\[2ex]
   622   \end{tabular}
   624   \begin{tabular}{lll}
   625   \<^bold>\<open>type\<close> \<open>session_build_args =\<close> \\
   626   \quad\<open>{session: string,\<close> \\
   627   \quad~~\<open>preferences?: string,\<close> & \<^bold>\<open>default:\<close> server preferences \\
   628   \quad~~\<open>options?: [string],\<close> \\
   629   \quad~~\<open>dirs?: [string],\<close> \\
   630   \quad~~\<open>ancestor_session?: string,\<close> \\
   631   \quad~~\<open>all_known?: bool,\<close> \\
   632   \quad~~\<open>focus_session?: bool,\<close> \\
   633   \quad~~\<open>required_session?: bool,\<close> \\
   634   \quad~~\<open>system_mode?: bool,\<close> \\
   635   \quad~~\<open>verbose?: bool}\<close> \\[2ex]
   637   \<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
   638   \quad\<open>{session: string,\<close> \\
   639   \quad~~\<open>ok: bool,\<close> \\
   640   \quad~~\<open>return_code: int,\<close> \\
   641   \quad~~\<open>timeout: bool,\<close> \\
   642   \quad~~\<open>timing: timing}\<close> \\[2ex]
   644   \<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
   645   \quad\<open>{ok: bool,\<close> \\
   646   \quad~~\<open>return_code: int,\<close> \\
   647   \quad~~\<open>sessions: [session_build_result]}\<close> \\
   648   \end{tabular}
   649 \<close>
   651 text \<open>
   652   The \<^verbatim>\<open>session_build\<close> command prepares a session image for interactive use of
   653   theories. This is a limited version of command-line tool @{tool build}
   654   (\secref{sec:tool-build}), with specific options to request a formal context
   655   for an interactive PIDE session.
   657   The build process is asynchronous, with notifications that inform about the
   658   progress of loaded theories. Some further informative messages are output as
   659   well.
   661   Coordination of independent build processes is at the discretion of the
   662   client (or end-user), just as for @{tool build} and @{tool jedit}. There is
   663   no built-in coordination of conflicting builds with overlapping hierarchies
   664   of session images. In the worst case, a session image produced by one task
   665   may get overwritten by another task!
   666 \<close>
   669 subsubsection \<open>Arguments\<close>
   671 text \<open>
   672   The \<open>session\<close> field is mandatory. It specifies the target session name:
   673   either directly (default) or indirectly (if \<open>required_session\<close> is \<^verbatim>\<open>true\<close>).
   674   The build process will produce all required ancestor images for the
   675   specified target.
   677   \<^medskip>
   678   The environment of Isabelle system options is determined from \<open>preferences\<close>
   679   that are augmented by \<open>options\<close>, which is a list individual updates of the
   680   form the \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> (the latter abbreviates
   681   \<open>name\<close>\<^verbatim>\<open>=true\<close>); see also command-line option \<^verbatim>\<open>-o\<close> for @{tool build}. The
   682   preferences are loaded from the file
   683   \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> by default, but the client may
   684   provide alternative contents for it (as text, not a file-name). This could
   685   be relevant in situations where client and server run in different
   686   operating-system contexts.
   688   \<^medskip>
   689   The \<open>dirs\<close> field specifies additional directories for session ROOT and ROOTS
   690   files (\secref{sec:session-root}). This augments the name space of available
   691   sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
   693   \<^medskip>
   694   The \<open>ancestor_session\<close> field specifies an alternative image as starting
   695   point for the target image. The default is to use the parent session
   696   according to the ROOT entry; see also option \<^verbatim>\<open>-A\<close> in @{tool jedit}. This
   697   can lead to a more light-weight build process, by skipping intermediate
   698   session images of the hierarchy that are not used later on.
   700   \<^medskip>
   701   The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all sessions from reachable
   702   ROOT entries into the name space of theories. This is relevant for proper
   703   session-qualified names, instead of referring to theory file names. The
   704   option enables the \<^verbatim>\<open>use_theories\<close> command
   705   (\secref{sec:command-use-theories}) to refer to arbitrary theories from
   706   other sessions, but considerable time is required to explore all accessible
   707   session directories and theory dependencies.
   709   \<^medskip>
   710   The \<open>focus_session\<close> field set to \<^verbatim>\<open>true\<close> focuses on the target session:
   711   the accessible name space of theories is restricted to sessions that are
   712   connected to it in the imports graph.
   714   \<^medskip>
   715   The \<open>required_session\<close> field set to \<^verbatim>\<open>true\<close> indicates that the target image
   716   should not be the \<open>session\<close>, but its parent (or ancestor according to
   717   \<open>ancestor_session\<close>). Thus it prepares a session context where theories from
   718   the \<open>session\<close> itself can be loaded.
   720   \<^medskip>
   721   The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
   722   log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
   723   @{setting ISABELLE_OUTPUT} (which is normally in @{setting
   724   ISABELLE_HOME_USER}). See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
   726   \<^medskip>
   727   The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
   728   similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
   729 \<close>
   732 subsubsection \<open>Intermediate output\<close>
   734 text \<open>
   735   The asynchronous notifications of command \<^verbatim>\<open>session_build\<close> mainly serve as
   736   progress indicator: the output resembles that of the session build window of
   737   Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
   739   For the client it is usually sufficient to print the messages in plain text,
   740   but note that \<open>theory_progress\<close> also reveals formal \<open>theory\<close> and
   741   \<open>session\<close> names directly.
   742 \<close>
   745 subsubsection \<open>Results\<close>
   747 text \<open>
   748   The overall \<open>session_build_results\<close> contain both a summary and an entry
   749   \<open>session_build_result\<close> for each session in the build hierarchy. The result
   750   is always provided, independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or
   751   failure (\<^verbatim>\<open>FAILED\<close> task).
   753   The \<open>ok\<close> field tells abstractly, whether all required session builds came
   754   out as \<open>ok\<close>, i.e.\ with zero \<open>return_code\<close>. A non-zero \<open>return_code\<close>
   755   indicates an error according to usual POSIX conventions for process exit.
   757   The individual \<open>session_build_result\<close> entries provide extra fields:
   759   \<^item> \<open>timeout\<close> tells if the build process was aborted after running too long,
   761   \<^item> \<open>timing\<close> gives the overall process timing in the usual Isabelle format
   762   with elapsed, CPU, GC time.
   763 \<close>
   766 subsubsection \<open>Examples\<close>
   768 text \<open>
   769   Build of a session image from the Isabelle distribution:
   770   @{verbatim [display] \<open>session_build {"session": "HOL-Word"}\<close>}
   772   Build a session image from the Archive of Formal Proofs:
   773   @{verbatim [display] \<open>session_build {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
   775   Build of a session image of \<^verbatim>\<open>HOL-Number_Theory\<close> directly on top of \<^verbatim>\<open>HOL\<close>:
   776   @{verbatim [display] \<open>session_build {"session": "HOL-Number_Theory", "ancestor_session": "HOL"}\<close>}
   777 \<close>
   780 subsection \<open>Command \<^verbatim>\<open>session_start\<close> \label{sec:command-session-start}\<close>
   782 text \<open>
   783   \begin{tabular}{lll}
   784   argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\
   785   immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   786   notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
   787   regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_start_result\<close> \\
   788   error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex]
   789   \end{tabular}
   791   \begin{tabular}{l}
   792   \<^bold>\<open>type\<close> \<open>session_start_result = {session: string, session_id: uuid}\<close>
   793   \end{tabular}
   795   \<^medskip>
   796   The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with
   797   underlying Isabelle/ML process, based on a session image that it produces on
   798   demand using \<^verbatim>\<open>session_build\<close>. Thus it accepts all \<open>session_build_args\<close> and
   799   produces similar notifications, but the detailed \<open>session_build_results\<close> are
   800   omitted.
   802   The session build and startup process is asynchronous: when the task is
   803   finished, the session remains active for commands, until a \<^verbatim>\<open>session_stop\<close>
   804   or \<^verbatim>\<open>shutdown\<close> command is sent to the server.
   806   Sessions are independent of client connections: it is possible to start a
   807   session and later apply \<^verbatim>\<open>use_theories\<close> on different connections, as long as
   808   the internal session identifier is known: shared theory imports will be used
   809   only once (and persist until purged explicitly).
   810 \<close>
   813 subsubsection \<open>Arguments\<close>
   815 text \<open>
   816   Most arguments are shared with \<^verbatim>\<open>session_build\<close>
   817   (\secref{sec:command-session-build}).
   819   \<^medskip>
   820   The \<open>print_mode\<close> field adds identifiers of print modes to be made active for
   821   this session. For example, \<^verbatim>\<open>"print_mode": ["ASCII"]\<close> prefers ASCII
   822   replacement syntax over mathematical Isabelle symbols. See also option \<^verbatim>\<open>-m\<close>
   823   in @{tool process} (\secref{sec:tool-process}).
   824 \<close>
   827 subsubsection \<open>Results\<close>
   829 text \<open>
   830   The \<open>session\<close> field provides the active session name for clarity.
   832   \<^medskip>
   833   The \<open>session_id\<close> field provides the internal identification of the session
   834   object within the sever process. It can remain active as long as the server
   835   is running, independently of the current client connection.
   836 \<close>
   839 subsection \<open>Examples\<close>
   841 text \<open>
   842   Start a default Isabelle/HOL session:
   843   @{verbatim [display] \<open>session_start {"session": "HOL"}\<close>}
   845   Start a session from the Archive of Formal Proofs:
   846   @{verbatim [display] \<open>session_start {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
   847 \<close>
   850 subsection \<open>Command \<^verbatim>\<open>session_stop\<close>\<close>
   852 text \<open>
   853   \begin{tabular}{ll}
   854   argument: & \<open>{session_id?: uuid}\<close> \\
   855   immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   856   regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_stop_result\<close> \\
   857   error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_stop_result\<close> \\[2ex]
   858   \end{tabular}
   860   \begin{tabular}{l}
   861   \<^bold>\<open>type\<close> \<open>session_stop_result = {ok: bool, return_code: int}\<close>
   862   \end{tabular}
   864   \<^medskip>
   865   The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified PIDE
   866   session. This asynchronous tasks usually finishes quickly. Failure only
   867   happens in unusual situations, according to the return code of the
   868   underlying Isabelle/ML process.
   869 \<close>
   872 subsubsection \<open>Arguments\<close>
   874 text \<open>
   875   The \<open>session_id\<close> field provides the UUID originally created by the server
   876   for this session.
   877 \<close>
   880 subsubsection \<open>Results\<close>
   882 text \<open>
   883   The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process has
   884   terminated properly.
   886   The \<open>return_code\<close> field expresses this information according to usual POSIX
   887   conventions for process exit.
   888 \<close>
   891 subsection \<open>Command \<^verbatim>\<open>use_theories\<close> \label{sec:command-use-theories}\<close>
   893 text \<open>
   894   \begin{tabular}{ll}
   895   argument: & \<open>use_theories_arguments\<close> \\
   896   regular result: & \<^verbatim>\<open>OK\<close> \<open>use_theories_results\<close> \\
   897   \end{tabular}
   899   \begin{tabular}{ll}
   900   \<^bold>\<open>type\<close> \<open>theory_name = string | {name: string, pos: position}\<close> \\
   901   \end{tabular}
   903   \begin{tabular}{ll}
   904   \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
   905   \quad\<open>{session_id: uuid,\<close> \\
   906   \quad~~\<open>theories: [theory_name],\<close> \\
   907   \quad~~\<open>qualifier?: string,\<close> \\
   908   \quad~~\<open>master_dir?: string,\<close> \\
   909   \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   910   \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
   911   \end{tabular}
   913   \begin{tabular}{ll}
   914   \<^bold>\<open>type\<close> \<open>node_result =\<close> \\
   915   \quad\<open>{node_name: string,\<close> \\
   916   \quad~~\<open>theory: string,\<close> \\
   917   \quad~~\<open>status: node_status,\<close> \\
   918   \quad~~\<open>messages: [message]}\<close> \\[2ex]
   920   \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
   921   \quad\<open>{ok: bool,\<close> \\
   922   \quad~~\<open>errors: [message],\<close> \\
   923   \quad~~\<open>nodes: [node_result]}\<close> \\[2ex]
   924   \end{tabular}
   926   \<^medskip>
   927   The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
   928   current version of theory files to it, while dependencies are resolved
   929   implicitly. The command succeeds eventually, when all theories have been
   930   \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
   931   (\secref{sec:json-types}): the outermost command structure has finished (or
   932   failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
   934   Already used theories persist in the session until purged explicitly. This
   935   also means that repeated invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it
   936   could make sense to do that with different values for \<open>pretty_margin\<close> or
   937   \<open>unicode_symbols\<close> to get different formatting for \<open>errors\<close> or \<open>messages\<close>.
   938 \<close>
   941 subsubsection \<open>Arguments\<close>
   943 text \<open>
   944   The \<open>session_id\<close> is the identifier provided by the server, when the session
   945   was created (possibly on a different client connection).
   947   \<^medskip>
   948   The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
   949   ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
   950   specifications may be given, which is occasionally useful for precise error
   951   locations.
   953   \<^medskip>
   954   The \<open>qualifier\<close> field provides an alternative session qualifier for theories
   955   that are not formally recognized as a member of a particular session. The
   956   default is \<^verbatim>\<open>Draft\<close> as in Isabelle/jEdit. There is rarely a need to change
   957   that, as theory nodes are already uniquely identified by their physical
   958   file-system location. This already allows reuse of theory base names with
   959   the same session qualifier --- as long as these theories are not used
   960   together (e.g.\ in \<^theory_text>\<open>imports\<close>).
   962   \<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
   963   the imported theory. Normally this is determined implicitly from the parent
   964   directory of the theory file.
   966   \<^medskip>
   967   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
   968   default is suitable for classic console output. Formatting happens at the
   969   end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.
   971   \<^medskip>
   972   The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> renders message output for direct
   973   output on a Unicode capable channel, ideally with the Isabelle fonts as in
   974   Isabelle/jEdit. The default is to keep the symbolic representation of
   975   Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead of its rendering as \<open>\<forall>\<close>. This means the
   976   client needs to perform its own rendering before presenting it to the
   977   end-user.
   978 \<close>
   981 subsubsection \<open>Results\<close>
   983 text \<open>
   984   The \<open>ok\<close> field indicates overall success of processing the specified
   985   theories with all their dependencies.
   987   When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively
   988   (including imported theories). The messages contain position information for
   989   the original theory nodes.
   991   \<^medskip>
   992   The \<open>nodes\<close> field provides detailed information about each imported theory
   993   node. The individual fields are as follows:
   995   \<^item> \<open>node_name\<close>: the physical name for the theory node, based on its
   996   file-system location;
   998   \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close>;
  1000   \<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
  1001   \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
  1003   \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
  1004   (\<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>, etc.).
  1005 \<close>
  1008 subsubsection \<open>Examples\<close>
  1010 text \<open>
  1011   Process some example theory from the Isabelle distribution, within the
  1012   context of an already started session for Isabelle/HOL (see also
  1013   \secref{sec:command-session-start}):
  1014   @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Isar_Examples/Drinker"]}\<close>}
  1016   \<^medskip>
  1017   Process some example theories that import other theories via
  1018   session-qualified theory names:
  1020   @{verbatim [display] \<open>session_start {"session": "HOL", "all_known": true}
  1021 use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
  1022 session_stop {"session_id": ...}\<close>}
  1024   The option \<open>all_known\<close> has been used here to the full name space of
  1025   session-qualified theory names accessible in this session. This is also the
  1026   default in Isabelle/jEdit, although it requires significant startup time.
  1028   \<^medskip>
  1029   Process some example theories in the context of their (single) parent
  1030   session:
  1032   @{verbatim [display] \<open>session_start {"session": "HOL-Library"}
  1033 use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
  1034 session_stop {"session_id": ...}\<close>}
  1035 \<close>
  1037 end