src/Doc/System/Server.thy
author wenzelm
Sat Sep 01 20:20:50 2018 +0200 (10 months ago)
changeset 68871 f5c76072db55
parent 68770 add44e2b8cb0
child 68881 d975449b266e
permissions -rw-r--r--
more explicit status for "canceled" command within theory node;
     1 (*:maxLineLen=78:*)
     2 
     3 theory Server
     4 imports Base
     5 begin
     6 
     7 chapter \<open>The Isabelle server\<close>
     8 
     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.
    16 
    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.
    22 
    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>
    27 
    28 
    29 section \<open>Command-line tools\<close>
    30 
    31 subsection \<open>Server \label{sec:tool-server}\<close>
    32 
    33 text \<open>
    34   The @{tool_def server} tool manages resident server processes:
    35   @{verbatim [display]
    36 \<open>Usage: isabelle server [OPTIONS]
    37 
    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)
    46 
    47   Manage resident Isabelle servers.\<close>}
    48 
    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}.
    59 
    60   Other server management operations are invoked via options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-x\<close>
    61   (see below).
    62 
    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.
    67 
    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.
    72 
    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.
    76 
    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.
    82 
    83   \<^medskip>
    84   Option \<^verbatim>\<open>-L\<close> specifies a log file for exceptional output of internal server
    85   and session operations.
    86 
    87   \<^medskip>
    88   Operation \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
    89   details.
    90 
    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>
    95 
    96 
    97 subsection \<open>Client \label{sec:tool-client}\<close>
    98 
    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]
   104 
   105   Options are:
   106     -n NAME      explicit server name
   107     -p PORT      explicit server port
   108 
   109   Console interaction for Isabelle server (with line-editor).\<close>}
   110 
   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.
   115 
   116   \<^medskip>
   117   Option \<^verbatim>\<open>-n\<close> specifies an explicit server name as in @{tool server}.
   118 
   119   \<^medskip>
   120   Option \<^verbatim>\<open>-p\<close> specifies an explicit server port as in @{tool server}.
   121 \<close>
   122 
   123 
   124 subsection \<open>Examples\<close>
   125 
   126 text \<open>
   127   Ensure that a particular server instance is running in the background:
   128   @{verbatim [display] \<open>isabelle server -n test &\<close>}
   129 
   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" = 127.0.0.1:4711 (password "XYZ")\<close>}
   134 
   135   \<^medskip>
   136   List available server processes:
   137   @{verbatim [display] \<open>isabelle server -l\<close>}
   138 
   139   \<^medskip>
   140   Connect the command-line client to the above test server:
   141   @{verbatim [display] \<open>isabelle client -n test\<close>}
   142 
   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:
   145 
   146   @{verbatim [display]
   147 \<open>echo 42
   148 echo [1, 2, 3]
   149 echo {"a": "text", "b": true, "c": 42}\<close>}
   150 
   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.
   153 
   154   \<^medskip>
   155   Exit the named server on the command-line:
   156   @{verbatim [display] \<open>isabelle server -n test -x\<close>}
   157 \<close>
   158 
   159 
   160 section \<open>Protocol messages \label{sec:server-protocol}\<close>
   161 
   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.
   170 
   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.
   180 
   181   \medskip Subsequently, the protocol message formats are described in further
   182   detail.
   183 \<close>
   184 
   185 
   186 subsection \<open>Byte messages\<close>
   187 
   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.
   193 
   194   Message boundaries are determined as follows:
   195 
   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.
   199 
   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.
   204 
   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>
   211 
   212 
   213 subsection \<open>Text messages\<close>
   214 
   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>https://utf8everywhere.org\<close>.\<close>
   220 
   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>
   225 
   226 
   227 subsection \<open>Input and output messages \label{sec:input-output-messages}\<close>
   228 
   229 text \<open>
   230   Server input and output messages have a uniform format as follows:
   231 
   232     \<^item> \<open>name argument\<close> such that:
   233 
   234     \<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
   235     ``\<^verbatim>\<open>_\<close>'', ``\<^verbatim>\<open>.\<close>'',
   236 
   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),
   240 
   241     \<^item> \<open>argument\<close> is the rest of the message without line terminator.
   242 
   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.
   247 
   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:
   252 
   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>
   256 
   257   \<^medskip>
   258   The \<open>argument\<close> format is uniform for both input and output messages:
   259 
   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>)
   263 
   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>https://www.json.org\<close> and unofficial explorations ``Parsing JSON is a
   267   Minefield'' \<^url>\<open>http://seriot.ch/parsing_json.php\<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.
   271 
   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>
   278 
   279 
   280 subsection \<open>Initial password exchange\<close>
   281 
   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.
   288 
   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>
   296 
   297 
   298 subsection \<open>Synchronous commands\<close>
   299 
   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).
   306 
   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>
   316 
   317 
   318 subsection \<open>Asynchronous commands\<close>
   319 
   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.
   327 
   328   These are the protocol exchanges for various cases of command task
   329   execution:
   330 
   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}
   342 
   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.
   347 
   348   The synchronous command \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> tells the specified task
   349   to terminate prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is
   350   not guaranteed: the cancel event may come too late or the running process
   351   may just ignore it.
   352 \<close>
   353 
   354 
   355 section \<open>Types for JSON values \label{sec:json-types}\<close>
   356 
   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:
   360 
   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>
   373 
   374   This is a simplified variation of TypeScript
   375   interfaces.\<^footnote>\<open>\<^url>\<open>https://www.typescriptlang.org/docs/handbook/interfaces.html\<close>\<close>
   376   The meaning of these types is specified wrt. the Isabelle/Scala
   377   implementation as follows.
   378 
   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.
   383 
   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.
   387 
   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.
   390 
   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>https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare\<close>.\<close>
   395 
   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.
   398 
   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>
   404 
   405   \<^item> Type \<open>string\<close> represents Unicode text; it corresponds to type \<^verbatim>\<open>String\<close> in
   406   Scala.
   407 
   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).
   411 
   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>.
   417 
   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.
   422 
   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.
   426 
   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>.
   431 
   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.
   434 
   435   \<^item> Parentheses \<open>(t)\<close> merely group type expressions syntactically.
   436 
   437 
   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>.
   441 
   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.
   445 
   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.
   450 
   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.
   455 
   456   \<^bigskip>
   457   Here are some common type definitions, for use in particular specifications
   458   of command arguments and results.
   459 
   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.
   468 
   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>,
   472   \<^verbatim>\<open>error\<close>.
   473 
   474   \<^item> \<^bold>\<open>type\<close>~\<open>error_message = {kind:\<close>~\<^verbatim>\<open>"error"\<close>\<open>, message: string}\<close> refers to
   475   error messages in particular. These occur routinely with \<^verbatim>\<open>ERROR\<close> or
   476   \<^verbatim>\<open>FAILED\<close> replies, but also as initial command syntax errors (which are
   477   omitted in the command specifications below).
   478 
   479   \<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
   480   string, session: string}\<close> reports formal progress in loading theories (e.g.\
   481   when building a session image). Apart from a regular output message, it also
   482   reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
   483   \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
   484   e.g.\ theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
   485 
   486   \<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
   487   common Isabelle timing information in seconds, usually with a precision of
   488   three digits after the point (whole milliseconds).
   489 
   490   \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
   491   as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
   492   \<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/UUID.html\<close>.\<close> Such
   493   identifiers are created as private random numbers of the server and only
   494   revealed to the client that creates a certain resource (e.g.\ task or
   495   session). A client may disclose this information for use in a different
   496   client connection: this allows to share sessions between multiple
   497   connections.
   498 
   499   Client commands need to provide syntactically wellformed UUIDs: this is
   500   trivial to achieve by using only identifiers that have been produced by the
   501   server beforehand.
   502 
   503   \<^item> \<^bold>\<open>type\<close>~\<open>task = {task: uuid}\<close> identifies a newly created asynchronous task
   504   and thus allows the client to control it by the \<^verbatim>\<open>cancel\<close> command. The same
   505   task identification is included in all messages produced by this task.
   506 
   507   \<^item> \<^bold>\<open>type\<close> \<open>session_id = {session_id: uuid}\<close> identifies a newly created PIDE
   508   session managed by the server. Sessions are independent of client
   509   connections and may be shared by different clients, as long as the internal
   510   session identifier is known.
   511 
   512   \<^item> \<^bold>\<open>type\<close> \<open>node = {node_name: string, theory_name: string}\<close> represents the
   513   internal node name of a theory. The \<open>node_name\<close> is derived from the
   514   canonical theory file-name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close> after
   515   normalization within the file-system). The \<open>theory_name\<close> is the
   516   session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
   517 
   518   \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
   519   int, warned: int, failed: int, finished: int, canceled: bool, initialized:
   520   bool, consolidated: bool}\<close> represents a formal theory node status of the
   521   PIDE document model. Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>,
   522   \<open>failed\<close>, \<open>finished\<close> account for individual commands within a theory node;
   523   \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>canceled\<close> flag tells if some
   524   command in the theory has been spontaneously canceled (by an Interrupt
   525   exception that could also indicate resource problems). The \<open>initialized\<close>
   526   flag indicates that the initial \<^theory_text>\<open>theory\<close> command has been processed. The
   527   \<open>consolidated\<close> flag indicates whether the outermost theory command structure
   528   has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked.
   529 \<close>
   530 
   531 
   532 section \<open>Server commands and results\<close>
   533 
   534 text \<open>
   535   Here follows an overview of particular Isabelle server commands with their
   536   results, which are usually represented as JSON values with types according
   537   to \secref{sec:json-types}. The general format of input and output messages
   538   is described in \secref{sec:input-output-messages}. The relevant
   539   Isabelle/Scala source files are:
   540 
   541   \<^medskip>
   542   \begin{tabular}{l}
   543   \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
   544   \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close> \\
   545   \<^file>\<open>$ISABELLE_HOME/src/Pure/General/json.scala\<close> \\
   546   \end{tabular}
   547 \<close>
   548 
   549 
   550 subsection \<open>Command \<^verbatim>\<open>help\<close>\<close>
   551 
   552 text \<open>
   553   \begin{tabular}{ll}
   554   regular result: & \<^verbatim>\<open>OK\<close> \<open>[string]\<close> \\
   555   \end{tabular}
   556   \<^medskip>
   557 
   558   The \<^verbatim>\<open>help\<close> command has no argument and returns the list of server command
   559   names. This is occasionally useful for interactive experimentation (see also
   560   @{tool client} in \secref{sec:tool-client}).
   561 \<close>
   562 
   563 
   564 subsection \<open>Command \<^verbatim>\<open>echo\<close>\<close>
   565 
   566 text \<open>
   567   \begin{tabular}{ll}
   568   argument: & \<open>any\<close> \\
   569   regular result: & \<^verbatim>\<open>OK\<close> \<open>any\<close> \\
   570   \end{tabular}
   571   \<^medskip>
   572 
   573   The \<^verbatim>\<open>echo\<close> command is the identity function: it returns its argument as
   574   regular result. This is occasionally useful for testing and interactive
   575   experimentation (see also @{tool client} in \secref{sec:tool-client}).
   576 
   577   The Scala type of \<^verbatim>\<open>echo\<close> is actually more general than given above:
   578   \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close> work uniformly. Note that \<^verbatim>\<open>XML.Elem\<close> might
   579   be difficult to type on the console in its YXML syntax
   580   (\secref{sec:yxml-vs-xml}).
   581 \<close>
   582 
   583 
   584 subsection \<open>Command \<^verbatim>\<open>shutdown\<close>\<close>
   585 
   586 text \<open>
   587   \begin{tabular}{ll}
   588   regular result: & \<^verbatim>\<open>OK\<close> \\
   589   \end{tabular}
   590   \<^medskip>
   591 
   592   The \<^verbatim>\<open>shutdown\<close> command has no argument and result value. It forces a
   593   shutdown of the connected server process, stopping all open sessions and
   594   closing the server socket. This may disrupt pending commands on other
   595   connections!
   596 
   597   \<^medskip>
   598   The command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server connection
   599   and issues a \<^verbatim>\<open>shutdown\<close> command (see also \secref{sec:tool-server}).
   600 \<close>
   601 
   602 
   603 subsection \<open>Command \<^verbatim>\<open>cancel\<close>\<close>
   604 
   605 text \<open>
   606   \begin{tabular}{ll}
   607   argument: & \<open>task\<close> \\
   608   regular result: & \<^verbatim>\<open>OK\<close> \\
   609   \end{tabular}
   610   \<^medskip>
   611 
   612   The command \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> attempts to cancel the specified
   613   task.
   614 
   615   Cancellation is merely a hint that the client prefers an ongoing process to
   616   be stopped. The command always succeeds formally, but it may get ignored by
   617   a task that is still running; it might also refer to a non-existing or
   618   no-longer existing task (without producing an error).
   619 
   620   Successful cancellation typically leads to an asynchronous failure of type
   621   \<^verbatim>\<open>FAILED {\<close>\<open>task: uuid, message:\<close>~\<^verbatim>\<open>"Interrupt"}\<close>. A different message is
   622   also possible, depending how the task handles the event.
   623 \<close>
   624 
   625 
   626 subsection \<open>Command \<^verbatim>\<open>session_build\<close> \label{sec:command-session-build}\<close>
   627 
   628 text \<open>
   629   \begin{tabular}{lll}
   630   argument: & \<open>session_build_args\<close> \\
   631   immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   632   notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
   633   regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_build_results\<close> \\
   634   error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_build_results\<close> \\[2ex]
   635   \end{tabular}
   636 
   637   \begin{tabular}{lll}
   638   \<^bold>\<open>type\<close> \<open>session_build_args =\<close> \\
   639   \quad\<open>{session: string,\<close> \\
   640   \quad~~\<open>preferences?: string,\<close> & \<^bold>\<open>default:\<close> server preferences \\
   641   \quad~~\<open>options?: [string],\<close> \\
   642   \quad~~\<open>dirs?: [string],\<close> \\
   643   \quad~~\<open>include_sessions: [string],\<close> \\
   644   \quad~~\<open>system_mode?: bool,\<close> \\
   645   \quad~~\<open>verbose?: bool}\<close> \\[2ex]
   646   \end{tabular}
   647 
   648   \begin{tabular}{ll}
   649   \<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
   650   \quad\<open>{session: string,\<close> \\
   651   \quad~~\<open>ok: bool,\<close> \\
   652   \quad~~\<open>return_code: int,\<close> \\
   653   \quad~~\<open>timeout: bool,\<close> \\
   654   \quad~~\<open>timing: timing}\<close> \\[2ex]
   655 
   656   \<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
   657   \quad\<open>{ok: bool,\<close> \\
   658   \quad~~\<open>return_code: int,\<close> \\
   659   \quad~~\<open>sessions: [session_build_result]}\<close> \\
   660   \end{tabular}
   661 \<close>
   662 
   663 text \<open>
   664   The \<^verbatim>\<open>session_build\<close> command prepares a session image for interactive use of
   665   theories. This is a limited version of command-line tool @{tool build}
   666   (\secref{sec:tool-build}), with specific options to request a formal context
   667   for an interactive PIDE session.
   668 
   669   The build process is asynchronous, with notifications that inform about the
   670   progress of loaded theories. Some further informative messages are output as
   671   well.
   672 
   673   Coordination of independent build processes is at the discretion of the
   674   client (or end-user), just as for @{tool build} and @{tool jedit}. There is
   675   no built-in coordination of conflicting builds with overlapping hierarchies
   676   of session images. In the worst case, a session image produced by one task
   677   may get overwritten by another task!
   678 \<close>
   679 
   680 
   681 subsubsection \<open>Arguments\<close>
   682 
   683 text \<open>
   684   The \<open>session\<close> field specifies the target session name. The build process
   685   will produce all required ancestor images according to the overall session
   686   graph.
   687 
   688   \<^medskip>
   689   The environment of Isabelle system options is determined from \<open>preferences\<close>
   690   that are augmented by \<open>options\<close>, which is a list individual updates of the
   691   form the \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> (the latter abbreviates
   692   \<open>name\<close>\<^verbatim>\<open>=true\<close>); see also command-line option \<^verbatim>\<open>-o\<close> for @{tool build}. The
   693   preferences are loaded from the file
   694   \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> by default, but the client may
   695   provide alternative contents for it (as text, not a file-name). This could
   696   be relevant in situations where client and server run in different
   697   operating-system contexts.
   698 
   699   \<^medskip>
   700   The \<open>dirs\<close> field specifies additional directories for session ROOT and ROOTS
   701   files (\secref{sec:session-root}). This augments the name space of available
   702   sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
   703 
   704   \<^medskip>
   705   The \<open>include_sessions\<close> field specifies sessions whose theories should be
   706   included in the overall name space of session-qualified theory names. This
   707   corresponds to a \<^bold>\<open>sessions\<close> specification in ROOT files
   708   (\secref{sec:session-root}). It enables the \<^verbatim>\<open>use_theories\<close> command
   709   (\secref{sec:command-use-theories}) to refer to sources from other sessions
   710   in a robust manner, instead of relying on directory locations.
   711 
   712   \<^medskip>
   713   If \<open>system_mode\<close> is \<^verbatim>\<open>true\<close>, session images are stored in @{path
   714   "$ISABELLE_HEAPS_SYSTEM"} instead of @{path "$ISABELLE_HEAPS"}. See also
   715   option \<^verbatim>\<open>-s\<close> in @{tool build} (\secref{sec:tool-build}).
   716 
   717   \<^medskip>
   718   The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
   719   similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
   720 \<close>
   721 
   722 
   723 subsubsection \<open>Intermediate output\<close>
   724 
   725 text \<open>
   726   The asynchronous notifications of command \<^verbatim>\<open>session_build\<close> mainly serve as
   727   progress indicator: the output resembles that of the session build window of
   728   Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
   729 
   730   For the client it is usually sufficient to print the messages in plain text,
   731   but note that \<open>theory_progress\<close> also reveals formal \<open>theory\<close> and
   732   \<open>session\<close> names directly.
   733 \<close>
   734 
   735 
   736 subsubsection \<open>Results\<close>
   737 
   738 text \<open>
   739   The overall \<open>session_build_results\<close> contain both a summary and an entry
   740   \<open>session_build_result\<close> for each session in the build hierarchy. The result
   741   is always provided, independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or
   742   failure (\<^verbatim>\<open>FAILED\<close> task).
   743 
   744   The \<open>ok\<close> field tells abstractly, whether all required session builds came
   745   out as \<open>ok\<close>, i.e.\ with zero \<open>return_code\<close>. A non-zero \<open>return_code\<close>
   746   indicates an error according to usual POSIX conventions for process exit.
   747 
   748   The individual \<open>session_build_result\<close> entries provide extra fields:
   749 
   750   \<^item> \<open>timeout\<close> tells if the build process was aborted after running too long,
   751 
   752   \<^item> \<open>timing\<close> gives the overall process timing in the usual Isabelle format
   753   with elapsed, CPU, GC time.
   754 \<close>
   755 
   756 
   757 subsubsection \<open>Examples\<close>
   758 
   759 text \<open>
   760   Build of a session image from the Isabelle distribution:
   761   @{verbatim [display] \<open>session_build {"session": "HOL-Word"}\<close>}
   762 
   763   Build a session image from the Archive of Formal Proofs:
   764   @{verbatim [display] \<open>session_build {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
   765 \<close>
   766 
   767 
   768 subsection \<open>Command \<^verbatim>\<open>session_start\<close> \label{sec:command-session-start}\<close>
   769 
   770 text \<open>
   771   \begin{tabular}{lll}
   772   argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\
   773   immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   774   notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
   775   regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id \<oplus> {tmp_dir: string}\<close> \\
   776   error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex]
   777   \end{tabular}
   778 
   779   \<^medskip>
   780   The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with
   781   underlying Isabelle/ML process, based on a session image that it produces on
   782   demand using \<^verbatim>\<open>session_build\<close>. Thus it accepts all \<open>session_build_args\<close> and
   783   produces similar notifications, but the detailed \<open>session_build_results\<close> are
   784   omitted.
   785 
   786   The session build and startup process is asynchronous: when the task is
   787   finished, the session remains active for commands, until a \<^verbatim>\<open>session_stop\<close>
   788   or \<^verbatim>\<open>shutdown\<close> command is sent to the server.
   789 
   790   Sessions are independent of client connections: it is possible to start a
   791   session and later apply \<^verbatim>\<open>use_theories\<close> on different connections, as long as
   792   the internal session identifier is known: shared theory imports will be used
   793   only once (and persist until purged explicitly).
   794 \<close>
   795 
   796 
   797 subsubsection \<open>Arguments\<close>
   798 
   799 text \<open>
   800   Most arguments are shared with \<^verbatim>\<open>session_build\<close>
   801   (\secref{sec:command-session-build}).
   802 
   803   \<^medskip>
   804   The \<open>print_mode\<close> field adds identifiers of print modes to be made active for
   805   this session. For example, \<^verbatim>\<open>"print_mode": ["ASCII"]\<close> prefers ASCII
   806   replacement syntax over mathematical Isabelle symbols. See also option \<^verbatim>\<open>-m\<close>
   807   in @{tool process} (\secref{sec:tool-process}).
   808 \<close>
   809 
   810 
   811 subsubsection \<open>Results\<close>
   812 
   813 text \<open>
   814   The \<open>session_id\<close> provides the internal identification of the session object
   815   within the sever process. It can remain active as long as the server is
   816   running, independently of the current client connection.
   817 
   818   \<^medskip>
   819   The \<open>tmp_dir\<close> field refers to a temporary directory that is specifically
   820   created for this session and deleted after it has been stopped. This may
   821   serve as auxiliary file-space for the \<^verbatim>\<open>use_theories\<close> command, but
   822   concurrent use requires some care in naming temporary files, e.g.\ by
   823   using sub-directories with globally unique names.
   824 
   825   As \<open>tmp_dir\<close> is the default \<open>master_dir\<close> for commands \<^verbatim>\<open>use_theories\<close> and
   826   \<^verbatim>\<open>purge_theories\<close>, theory files copied there may be used without further
   827   path specification.
   828 \<close>
   829 
   830 
   831 subsubsection \<open>Examples\<close>
   832 
   833 text \<open>
   834   Start a default Isabelle/HOL session:
   835   @{verbatim [display] \<open>session_start {"session": "HOL"}\<close>}
   836 
   837   Start a session from the Archive of Formal Proofs:
   838   @{verbatim [display] \<open>session_start {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
   839 \<close>
   840 
   841 
   842 subsection \<open>Command \<^verbatim>\<open>session_stop\<close>\<close>
   843 
   844 text \<open>
   845   \begin{tabular}{ll}
   846   argument: & \<open>session_id\<close> \\
   847   immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   848   regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_stop_result\<close> \\
   849   error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_stop_result\<close> \\[2ex]
   850   \end{tabular}
   851 
   852   \begin{tabular}{l}
   853   \<^bold>\<open>type\<close> \<open>session_stop_result = {ok: bool, return_code: int}\<close>
   854   \end{tabular}
   855 
   856   \<^medskip>
   857   The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified PIDE
   858   session. This asynchronous tasks usually finishes quickly. Failure only
   859   happens in unusual situations, according to the return code of the
   860   underlying Isabelle/ML process.
   861 \<close>
   862 
   863 
   864 subsubsection \<open>Arguments\<close>
   865 
   866 text \<open>
   867   The \<open>session_id\<close> provides the UUID originally created by the server for this
   868   session.
   869 \<close>
   870 
   871 
   872 subsubsection \<open>Results\<close>
   873 
   874 text \<open>
   875   The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process has
   876   terminated properly.
   877 
   878   The \<open>return_code\<close> field expresses this information according to usual POSIX
   879   conventions for process exit.
   880 \<close>
   881 
   882 
   883 subsection \<open>Command \<^verbatim>\<open>use_theories\<close> \label{sec:command-use-theories}\<close>
   884 
   885 text \<open>
   886   \begin{tabular}{ll}
   887   argument: & \<open>use_theories_arguments\<close> \\
   888   immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
   889   regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>use_theories_results\<close> \\
   890   \end{tabular}
   891 
   892   \begin{tabular}{ll}
   893   \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
   894   \quad\<open>{session_id: uuid,\<close> \\
   895   \quad~~\<open>theories: [string],\<close> \\
   896   \quad~~\<open>master_dir?: string,\<close> & \<^bold>\<open>default:\<close> session \<open>tmp_dir\<close> \\
   897   \quad~~\<open>pretty_margin?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   898   \quad~~\<open>unicode_symbols?: bool,\<close> \\
   899   \quad~~\<open>export_pattern?: string,\<close> \\
   900   \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
   901   \quad~~\<open>check_limit?: int,\<close> \\
   902   \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
   903   \end{tabular}
   904 
   905   \begin{tabular}{ll}
   906   \<^bold>\<open>type\<close> \<open>export =\<close> \\
   907   \quad~~\<open>{name: string, base64: bool, body: string}\<close> \\
   908   \<^bold>\<open>type\<close> \<open>node_results =\<close> \\
   909   \quad~~\<open>{status: node_status, messages: [message], exports: [export]}\<close> \\
   910   \<^bold>\<open>type\<close> \<open>nodes_status =\<close> \\
   911   \quad~~\<open>[node \<oplus> {status: node_status}]\<close> \\
   912   \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
   913   \quad\<open>{ok: bool,\<close> \\
   914   \quad~~\<open>errors: [message],\<close> \\
   915   \quad~~\<open>nodes: [node \<oplus> node_results]}\<close> \\
   916   \end{tabular}
   917 
   918   \<^medskip>
   919   The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
   920   current version of theory files to it, while dependencies are resolved
   921   implicitly. The command succeeds eventually, when all theories have been
   922   \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
   923   (\secref{sec:json-types}): the outermost command structure has finished (or
   924   failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
   925 
   926   Already used theories persist in the session until purged explicitly
   927   (\secref{sec:command-purge-theories}). This also means that repeated
   928   invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it could make sense to do
   929   that with different values for \<open>pretty_margin\<close> or \<open>unicode_symbols\<close> to get
   930   different formatting for \<open>errors\<close> or \<open>messages\<close>.
   931 
   932   \<^medskip> A non-empty \<open>export_pattern\<close> means that theory \<open>exports\<close> are retrieved
   933   (see \secref{sec:tool-export}). An \<open>export\<close> \<open>name\<close> roughly follows
   934   file-system standards: ``\<^verbatim>\<open>/\<close>'' separated list of base names (excluding
   935   special names like ``\<^verbatim>\<open>.\<close>'' or ``\<^verbatim>\<open>..\<close>''). The \<open>base64\<close> field specifies the
   936   format of the \<open>body\<close> string: it is true for a byte vector that cannot be
   937   represented as plain text in UTF-8 encoding, which means the string needs to
   938   be decoded as in \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
   939 
   940   \<^medskip> Due to asynchronous nature of PIDE document processing, structurally
   941   broken theories never reach the \<open>consolidated\<close> state: consequently
   942   \<^verbatim>\<open>use_theories\<close> will wait forever. The status is checked every \<open>check_delay\<close>
   943   seconds, and bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\
   944   unbounded). A \<open>check_limit > 0\<close> effectively specifies a timeout of
   945   \<open>check_delay \<times> check_limit\<close> seconds; it needs to be greater than the system
   946   option @{system_option editor_consolidate_delay} to give PIDE processing a
   947   chance to consolidate document nodes in the first place.
   948 
   949   \<^medskip> A non-negative \<open>nodes_status_delay\<close> enables continuous notifications of
   950   kind \<open>nodes_status\<close>, with a field of name and type \<open>nodes_status\<close>. The time
   951   interval is specified in seconds; by default it is negative and thus
   952   disabled.
   953 \<close>
   954 
   955 
   956 subsubsection \<open>Arguments\<close>
   957 
   958 text \<open>
   959   The \<open>session_id\<close> is the identifier provided by the server, when the session
   960   was created (possibly on a different client connection).
   961 
   962   \<^medskip>
   963   The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
   964   ROOT \<^bold>\<open>theories\<close>.
   965 
   966   \<^medskip>
   967   The \<open>master_dir\<close> field specifies the master directory of imported theories:
   968   it acts like the ``current working directory'' for locating theory files.
   969   This is irrelevant for \<open>theories\<close> with an absolute path name (e.g.\
   970   \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
   971   \<^verbatim>\<open>"HOL-ex/Seq"\<close>).
   972 
   973   \<^medskip>
   974   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
   975   default is suitable for classic console output. Formatting happens at the
   976   end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.
   977 
   978   \<^medskip>
   979   The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> renders message output for direct
   980   output on a Unicode capable channel, ideally with the Isabelle fonts as in
   981   Isabelle/jEdit. The default is to keep the symbolic representation of
   982   Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead of its rendering as \<open>\<forall>\<close>. This means the
   983   client needs to perform its own rendering before presenting it to the
   984   end-user.
   985 \<close>
   986 
   987 
   988 subsubsection \<open>Results\<close>
   989 
   990 text \<open>
   991   The \<open>ok\<close> field indicates overall success of processing the specified
   992   theories with all their dependencies.
   993 
   994   When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively
   995   (including imported theories). The messages contain position information for
   996   the original theory nodes.
   997 
   998   \<^medskip>
   999   The \<open>nodes\<close> field provides detailed information about each imported theory
  1000   node. The individual fields are as follows:
  1001 
  1002   \<^item> \<open>node_name\<close>: the canonical name for the theory node, based on its
  1003   file-system location;
  1004 
  1005   \<^item> \<open>theory_name\<close>: the logical theory name;
  1006 
  1007   \<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
  1008   \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
  1009 
  1010   \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
  1011   (with kind \<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>).
  1012 \<close>
  1013 
  1014 
  1015 subsubsection \<open>Examples\<close>
  1016 
  1017 text \<open>
  1018   Process some example theory from the Isabelle distribution, within the
  1019   context of an already started session for Isabelle/HOL (see also
  1020   \secref{sec:command-session-start}):
  1021   @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/ex/Seq"]}\<close>}
  1022 
  1023   \<^medskip>
  1024   Process some example theories in the context of their (single) parent
  1025   session:
  1026 
  1027   @{verbatim [display] \<open>session_start {"session": "HOL-Library"}
  1028 use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
  1029 session_stop {"session_id": ...}\<close>}
  1030 
  1031   \<^medskip>
  1032   Process some example theories that import other theories via
  1033   session-qualified theory names:
  1034 
  1035   @{verbatim [display] \<open>session_start {"session": "HOL", "include_sessions": ["HOL-Unix"]}
  1036 use_theories {"session_id": ..., "theories": ["HOL-Unix.Unix"]}
  1037 session_stop {"session_id": ...}\<close>}
  1038 \<close>
  1039 
  1040 
  1041 subsection \<open>Command \<^verbatim>\<open>purge_theories\<close> \label{sec:command-purge-theories}\<close>
  1042 
  1043 text \<open>
  1044   \begin{tabular}{ll}
  1045   argument: & \<open>purge_theories_arguments\<close> \\
  1046   regular result: & \<^verbatim>\<open>OK\<close> \<open>purge_theories_result\<close> \\
  1047   \end{tabular}
  1048 
  1049   \begin{tabular}{lll}
  1050   \<^bold>\<open>type\<close> \<open>purge_theories_arguments =\<close> \\
  1051   \quad\<open>{session_id: uuid,\<close> \\
  1052   \quad~~\<open>theories: [string],\<close> \\
  1053   \quad~~\<open>master_dir?: string,\<close> & \<^bold>\<open>default:\<close> session \<open>tmp_dir\<close> \\
  1054   \quad~~\<open>all?: bool}\<close> \\[2ex]
  1055   \end{tabular}
  1056 
  1057   \begin{tabular}{ll}
  1058   \<^bold>\<open>type\<close> \<open>purge_theories_result = {purged: [string]}\<close> \\
  1059   \end{tabular}
  1060 
  1061   \<^medskip>
  1062   The \<^verbatim>\<open>purge_theories\<close> command updates the identified session by removing
  1063   theories that are no longer required: theories that are used in pending
  1064   \<^verbatim>\<open>use_theories\<close> tasks or imported by other theories are retained.
  1065 \<close>
  1066 
  1067 
  1068 subsubsection \<open>Arguments\<close>
  1069 
  1070 text \<open>
  1071   The \<open>session_id\<close> is the identifier provided by the server, when the session
  1072   was created (possibly on a different client connection).
  1073 
  1074   \<^medskip>
  1075   The \<open>theories\<close> field specifies theory names to be purged: imported
  1076   dependencies are \<^emph>\<open>not\<close> completed. Instead it is possible to provide the
  1077   already completed import graph returned by \<^verbatim>\<open>use_theories\<close> as \<open>nodes\<close> /
  1078   \<open>node_name\<close>.
  1079 
  1080   \<^medskip>
  1081   The \<open>master_dir\<close> field specifies the master directory as in \<^verbatim>\<open>use_theories\<close>.
  1082   This is irrelevant, when passing fully-qualified theory node names (e.g.\
  1083   \<open>node_name\<close> from \<open>nodes\<close> in \<open>use_theories_results\<close>).
  1084 
  1085   \<^medskip>
  1086   The \<open>all\<close> field set to \<^verbatim>\<open>true\<close> attempts to purge all presently loaded
  1087   theories.
  1088 \<close>
  1089 
  1090 
  1091 subsubsection \<open>Results\<close>
  1092 
  1093 text \<open>
  1094   The \<open>purged\<close> field gives the theory nodes that were actually removed.
  1095 
  1096   \<^medskip>
  1097   The \<open>retained\<close> field gives the remaining theory nodes, i.e.\ the complement
  1098   of \<open>purged\<close>.
  1099 \<close>
  1100 
  1101 end