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