documentation for the Isabelle server;
authorwenzelm
Mon Mar 19 19:24:45 2018 +0100 (14 months ago)
changeset 67904465f43a9f780
parent 67903 6e85d866251f
child 67905 fe0f4eeceeb7
documentation for the Isabelle server;
NEWS
lib/Tools/client
src/Doc/ROOT
src/Doc/System/Environment.thy
src/Doc/System/Server.thy
src/Doc/System/document/root.tex
src/Pure/Tools/server.scala
     1.1 --- a/NEWS	Mon Mar 19 18:13:37 2018 +0100
     1.2 +++ b/NEWS	Mon Mar 19 19:24:45 2018 +0100
     1.3 @@ -267,6 +267,11 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 +* The command-line tools "isabelle server" and "isabelle client" provide
     1.8 +access to the Isabelle Server: it supports responsive session management
     1.9 +and concurrent use of theories, based on Isabelle/PIDE infrastructure.
    1.10 +See also the "system" manual.
    1.11 +
    1.12  * The command-line tool "isabelle update_comments" normalizes formal
    1.13  comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
    1.14  approximate the appearance in document output). This is more specific
     2.1 --- a/lib/Tools/client	Mon Mar 19 18:13:37 2018 +0100
     2.2 +++ b/lib/Tools/client	Mon Mar 19 19:24:45 2018 +0100
     2.3 @@ -2,7 +2,7 @@
     2.4  #
     2.5  # Author: Makarius
     2.6  #
     2.7 -# DESCRIPTION: console interaction for Isabelle server (with line-editor)
     2.8 +# DESCRIPTION: console interaction for Isabelle servers (with line-editor)
     2.9  
    2.10  PRG="$(basename "$0")"
    2.11  
    2.12 @@ -15,7 +15,7 @@
    2.13    echo "    -n NAME      explicit server name"
    2.14    echo "    -p PORT      explicit server port"
    2.15    echo
    2.16 -  echo "  Console interaction for Isabelle server (with line-editor)."
    2.17 +  echo "  Console interaction for Isabelle servers (with line-editor)."
    2.18    echo
    2.19    exit 1
    2.20  }
     3.1 --- a/src/Doc/ROOT	Mon Mar 19 18:13:37 2018 +0100
     3.2 +++ b/src/Doc/ROOT	Mon Mar 19 19:24:45 2018 +0100
     3.3 @@ -378,6 +378,7 @@
     3.4      Environment
     3.5      Sessions
     3.6      Presentation
     3.7 +    Server
     3.8      Scala
     3.9      Misc
    3.10    document_files (in "..")
     4.1 --- a/src/Doc/System/Environment.thy	Mon Mar 19 18:13:37 2018 +0100
     4.2 +++ b/src/Doc/System/Environment.thy	Mon Mar 19 19:24:45 2018 +0100
     4.3 @@ -469,7 +469,7 @@
     4.4  \<close>
     4.5  
     4.6  
     4.7 -section \<open>YXML versus XML\<close>
     4.8 +section \<open>YXML versus XML \label{sec:yxml-vs-xml}\<close>
     4.9  
    4.10  text \<open>
    4.11    Isabelle tools often use YXML, which is a simple and efficient syntax for
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Doc/System/Server.thy	Mon Mar 19 19:24:45 2018 +0100
     5.3 @@ -0,0 +1,354 @@
     5.4 +(*:maxLineLen=78:*)
     5.5 +
     5.6 +theory Server
     5.7 +imports Base
     5.8 +begin
     5.9 +
    5.10 +chapter \<open>The Isabelle server\<close>
    5.11 +
    5.12 +text \<open>
    5.13 +  An Isabelle session requires at least two processes, which are both rather
    5.14 +  heavy: Isabelle/Scala for the system infrastructure and Isabelle/ML for the
    5.15 +  logic session (e.g.\ HOL). In principle, these processes can be invoked
    5.16 +  directly on the command-line, e.g.\ via @{tool java}, @{tool scala}, @{tool
    5.17 +  process}, @{tool console}, but this approach is inadequate for reactive
    5.18 +  applications that require quick responses from the prover.
    5.19 +
    5.20 +  In contrast, the Isabelle server exposes Isabelle/Scala as a
    5.21 +  ``terminate-stay-resident'' application that manages multiple logic
    5.22 +  \<^emph>\<open>sessions\<close> and concurrent tasks to use \<^emph>\<open>theories\<close>. This provides an
    5.23 +  analogous to @{ML Thy_Info.use_theories} in Isabelle/ML, but with full
    5.24 +  concurrency and Isabelle/PIDE markup.
    5.25 +
    5.26 +  The client/server arrangement via TCP sockets also opens possibilities for
    5.27 +  remote Isabelle services that are accessed by local applications, e.g.\ via
    5.28 +  an SSH tunnel.
    5.29 +\<close>
    5.30 +
    5.31 +
    5.32 +section \<open>Command-line tools\<close>
    5.33 +
    5.34 +subsection \<open>Server \label{sec:tool-server}\<close>
    5.35 +
    5.36 +text \<open>
    5.37 +  The @{tool_def server} tool manages resident server processes:
    5.38 +  @{verbatim [display]
    5.39 +\<open>Usage: isabelle server [OPTIONS]
    5.40 +
    5.41 +  Options are:
    5.42 +    -L FILE      logging on FILE
    5.43 +    -c           console interaction with specified server
    5.44 +    -l           list servers (alternative operation)
    5.45 +    -n NAME      explicit server name (default: isabelle)
    5.46 +    -p PORT      explicit server port
    5.47 +    -s           assume existing server, no implicit startup
    5.48 +    -x           exit specified server (alternative operation)
    5.49 +
    5.50 +  Manage resident Isabelle servers.\<close>}
    5.51 +
    5.52 +  The main operation of \<^verbatim>\<open>isabelle server\<close> is to ensure that a named server is
    5.53 +  running, either by finding an already running process (according to the
    5.54 +  central database file @{path "$ISABELLE_HOME_USER/servers.db"}) or by
    5.55 +  becoming itself a new server that accepts connections on a particular TCP
    5.56 +  socket. The server name and its address are printed as initial output line.
    5.57 +  If another server instance is already running, the current
    5.58 +  \<^verbatim>\<open>isabelle server\<close> process will terminate; otherwise, it keeps running as a
    5.59 +  new server process until an explicit \<^verbatim>\<open>shutdown\<close> command is received.
    5.60 +  Further details of the server socket protocol are explained in
    5.61 +  \secref{sec:server-protocol}.
    5.62 +
    5.63 +  Other server management operations are invoked via options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-x\<close>
    5.64 +  (see below).
    5.65 +
    5.66 +  \<^medskip>
    5.67 +  Option \<^verbatim>\<open>-n\<close> specifies an alternative server name: at most one process for
    5.68 +  each name may run, but each server instance supports multiple connections
    5.69 +  and logic sessions.
    5.70 +
    5.71 +  \<^medskip>
    5.72 +  Option \<^verbatim>\<open>-p\<close> specifies an explicit TCP port for the server socket (which is
    5.73 +  always on \<^verbatim>\<open>localhost\<close>): the default is to let the operating system assign a
    5.74 +  free port number.
    5.75 +
    5.76 +  \<^medskip>
    5.77 +  Option \<^verbatim>\<open>-s\<close> strictly assumes that the specified server process is already
    5.78 +  running, skipping the optional server startup phase.
    5.79 +
    5.80 +  \<^medskip>
    5.81 +  Option \<^verbatim>\<open>-c\<close> connects the console in/out channels after the initial check
    5.82 +  for a suitable server process. Note that the @{tool client} tool
    5.83 +  (\secref{sec:tool-client}) provides a more convenient way to do this
    5.84 +  interactively, together with command-line editor support.
    5.85 +
    5.86 +  \<^medskip>
    5.87 +  Option \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
    5.88 +  details.
    5.89 +
    5.90 +  \<^medskip>
    5.91 +  Option \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a \<^verbatim>\<open>shutdown\<close>
    5.92 +  command.
    5.93 +
    5.94 +  \<^medskip>
    5.95 +  Option \<^verbatim>\<open>-L\<close> specifies a log file for exceptional output of internal server
    5.96 +  and session operations.
    5.97 +\<close>
    5.98 +
    5.99 +
   5.100 +subsection \<open>Client \label{sec:tool-client}\<close>
   5.101 +
   5.102 +text \<open>
   5.103 +  The @{tool_def client} provides console interaction for Isabelle servers:
   5.104 +  @{verbatim [display]
   5.105 +\<open>Usage: isabelle client [OPTIONS]
   5.106 +
   5.107 +  Options are:
   5.108 +    -n NAME      explicit server name
   5.109 +    -p PORT      explicit server port
   5.110 +
   5.111 +  Console interaction for Isabelle server (with line-editor).\<close>}
   5.112 +
   5.113 +  This is a convenient wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
   5.114 +  experimentation, wrapped into @{setting ISABELLE_LINE_EDITOR} if available.
   5.115 +  The server name is sufficient for identification, as the client can
   5.116 +  determine the connection details from the local database of active servers.
   5.117 +
   5.118 +  \<^medskip>
   5.119 +  Option \<^verbatim>\<open>-n\<close> specifies an explicit server name as in @{tool server}.
   5.120 +
   5.121 +  \<^medskip>
   5.122 +  Option \<^verbatim>\<open>-p\<close> specifies an explicit server port as in @{tool server}.
   5.123 +\<close>
   5.124 +
   5.125 +
   5.126 +subsection \<open>Examples\<close>
   5.127 +
   5.128 +text \<open>
   5.129 +  Ensure that a particular server instance is running in the background:
   5.130 +  @{verbatim [display] \<open>isabelle server -n test &\<close>}
   5.131 +
   5.132 +  Here the first line of output presents the connection details:\<^footnote>\<open>This
   5.133 +  information may be used in an independent TCP client, while the
   5.134 +  Isabelle/Scala tool merely needs the server name to access the database of
   5.135 +  servers.\<close>
   5.136 +  @{verbatim [display] \<open>server "test" = 127.0.0.1:4711 (password "XYZ")\<close>}
   5.137 +
   5.138 +  \<^medskip>
   5.139 +  List available server processes:
   5.140 +  @{verbatim [display] \<open>isabelle server -l\<close>}
   5.141 +
   5.142 +  \<^medskip>
   5.143 +  Connect the command-line client to the above test server:
   5.144 +  @{verbatim [display] \<open>isabelle client -n test\<close>}
   5.145 +
   5.146 +  Interaction now works on a line-by-line basis, with commands like \<^verbatim>\<open>help\<close> or
   5.147 +  \<^verbatim>\<open>echo\<close>. For example, some JSON values may be echoed like this:
   5.148 +
   5.149 +  @{verbatim [display]
   5.150 +\<open>echo 42
   5.151 +echo [1, 2, 3]
   5.152 +echo {"a": "text", "b": true, "c": 42}\<close>}
   5.153 +
   5.154 +  Closing the connection (via CTRL-D) leaves the server running: it is
   5.155 +  possible to reconnect again, and have multiple connections at the same time.
   5.156 +
   5.157 +  \<^medskip>
   5.158 +  Finally, exit the named server on the command-line:
   5.159 +  @{verbatim [display] \<open>isabelle server -n test -x\<close>}
   5.160 +\<close>
   5.161 +
   5.162 +
   5.163 +section \<open>Protocol messages \label{sec:server-protocol}\<close>
   5.164 +
   5.165 +text \<open>
   5.166 +  The Isabelle server listens on a regular TCP socket, using a line-oriented
   5.167 +  protocol of structured messages: input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
   5.168 +  (via \<^verbatim>\<open>OK\<close> or \<^verbatim>\<open>ERROR\<close>) are strictly alternating on the toplevel, but
   5.169 +  commands may also return a \<^emph>\<open>task\<close> identifier to indicate an ongoing
   5.170 +  asynchronous process that is joined later (via \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>).
   5.171 +  Asynchronous \<^verbatim>\<open>NOTE\<close> messages may occur at any time: they are independent of
   5.172 +  the main command-reply protocol.
   5.173 +
   5.174 +  For example, the synchronous \<^verbatim>\<open>echo\<close> command immediately returns its
   5.175 +  argument as \<^verbatim>\<open>OK\<close> result. In contrast, the asynchronous \<^verbatim>\<open>session_build\<close>
   5.176 +  command returns \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> and continues in the background. It
   5.177 +  will eventually produce \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> or
   5.178 +  \<^verbatim>\<open>FAILED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> with the final result. Intermediately, it
   5.179 +  may emit asynchronous messages of the form \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>
   5.180 +  to inform about its progress. Due to the explicit task identifier, the
   5.181 +  client can show these messages in the proper context, e.g.\ a GUI window for
   5.182 +  the session build job.
   5.183 +
   5.184 +  \medskip Subsequently, the protocol message formats are described in further
   5.185 +  detail.
   5.186 +\<close>
   5.187 +
   5.188 +
   5.189 +subsection \<open>Byte messages\<close>
   5.190 +
   5.191 +text \<open>
   5.192 +  The client-server connection is a raw byte-channel for bidirectional
   5.193 +  communication, but the Isabelle server always works with messages of a
   5.194 +  particular length. Messages are written as a single chunk that is flushed
   5.195 +  immediately.
   5.196 +
   5.197 +  The message boundary is determined as follows:
   5.198 +
   5.199 +    \<^item> A \<^emph>\<open>short message\<close> consists of a single line: it is a sequence of
   5.200 +    arbitrary bytes excluding CR (13) and LF (10), and terminated by CR-LF or
   5.201 +    just LF.
   5.202 +
   5.203 +    \<^item> A \<^emph>\<open>long message\<close> starts with a single line as above, which consists
   5.204 +    only of decimal digits: that is interpreted as length of the subsequent
   5.205 +    block of arbitrary bytes. A final line-terminator may be included here,
   5.206 +    but is not required.
   5.207 +
   5.208 +  Messages in JSON format (see below) always fit on a single line, due to
   5.209 +  escaping of newline characters within string literals. This is convenient
   5.210 +  for interactive experimentation, but it can impact performance for very long
   5.211 +  messages. If the message byte-length is given on the preceding line, the
   5.212 +  server can read the message efficiently as a single block.
   5.213 +\<close>
   5.214 +
   5.215 +
   5.216 +subsection \<open>Text messages\<close>
   5.217 +
   5.218 +text \<open>
   5.219 +  Messages are read and written as byte streams (with byte lengths), but the
   5.220 +  content is always interpreted as plain text in terms of the UTF-8
   5.221 +  encoding.\<^footnote>\<open>See also the ``UTF-8 Everywhere Manifesto''
   5.222 +  \<^url>\<open>http://utf8everywhere.org\<close>.\<close>
   5.223 +
   5.224 +  Note that line-endings and other formatting characters are invariant wrt.
   5.225 +  UTF-8 representation of text: thus implementations are free to determine the
   5.226 +  overall message structure before or after applying the text encoding.
   5.227 +\<close>
   5.228 +
   5.229 +
   5.230 +subsection \<open>Input and output messages\<close>
   5.231 +
   5.232 +text \<open>
   5.233 +  Server input and output messages have a uniform format as follows:
   5.234 +
   5.235 +    \<^item> \<open>name argument\<close> such that:
   5.236 +
   5.237 +    \<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
   5.238 +    ``\<^verbatim>\<open>_\<close>'' (underscore), or ``\<^verbatim>\<open>.\<close>'' (dot),
   5.239 +
   5.240 +    \<^item> the separator between \<open>name\<close> and \<open>argument\<close> is the longest possible
   5.241 +    sequence of ASCII blanks (it could be empty, e.g.\ when the argument
   5.242 +    starts with a quote or bracket),
   5.243 +
   5.244 +    \<^item> \<open>argument\<close> is the rest of the message without the line terminator.
   5.245 +
   5.246 +  \<^medskip>
   5.247 +  Input messages are sent from the client to the server. Here the \<open>name\<close>
   5.248 +  specifies a \<^emph>\<open>server command\<close>: the list of known commands may be
   5.249 +  retrieved via the \<^verbatim>\<open>help\<close> command.
   5.250 +
   5.251 +  \<^medskip>
   5.252 +  Output messages are sent from the server to the client. Here the \<open>name\<close>
   5.253 +  specifies the \<^emph>\<open>server reply\<close>, which always has a specific meaning as
   5.254 +  follows:
   5.255 +
   5.256 +    \<^item> synchronous results: \<^verbatim>\<open>OK\<close> or \<^verbatim>\<open>ERROR\<close>
   5.257 +    \<^item> asynchronous results: \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>
   5.258 +    \<^item> intermediate notifications: \<^verbatim>\<open>NOTE\<close>
   5.259 +
   5.260 +  \<^medskip>
   5.261 +  The \<open>argument\<close> format is uniform for both input and output messages:
   5.262 +
   5.263 +    \<^item> empty argument (Scala type \<^verbatim>\<open>Unit\<close>)
   5.264 +    \<^item> XML element in YXML notation (Scala type \<^verbatim>\<open>XML.Elem\<close>)
   5.265 +    \<^item> JSON value (Scala type \<^verbatim>\<open>JSON.T\<close>)
   5.266 +
   5.267 +  JSON values may consist of objects (records), arrays (lists), strings,
   5.268 +  numbers, bools, null.\<^footnote>\<open>See also the official specification
   5.269 +  \<^url>\<open>https://www.json.org\<close> and unofficial explorations ``Parsing JSON is a
   5.270 +  Minefield'' \<^url>\<open>http://seriot.ch/parsing_json.php\<close>.\<close> Since JSON requires
   5.271 +  explicit quotes and backslash-escapes to represent arbitrary text, the YXML
   5.272 +  notation for XML trees (\secref{sec:yxml-vs-xml}) works better
   5.273 +  for large messages with a lot of PIDE markup.
   5.274 +
   5.275 +  Nonetheless, the most common commands use JSON by default: big chunks of
   5.276 +  text (theory sources etc.) are taken from the underlying file-system and
   5.277 +  results are pre-formatted for plain-text output, without PIDE markup
   5.278 +  information. This is a concession to simplicity: the server imitates the
   5.279 +  appearance of command-line tools on top of the Isabelle/PIDE infrastructure.
   5.280 +\<close>
   5.281 +
   5.282 +
   5.283 +subsection \<open>Initial password exchange\<close>
   5.284 +
   5.285 +text \<open>
   5.286 +  Whenever a new client opens the server socket, the initial message needs to
   5.287 +  be its unique password. The server replies either with \<^verbatim>\<open>OK\<close> (and some
   5.288 +  information about the Isabelle version) or by silent disconnection of what
   5.289 +  is considered an illegal connection attempt.
   5.290 +
   5.291 +  Server passwords are created as Universally Unique Identifier (UUID) in
   5.292 +  Isabelle/Scala and stored in a per-user database, with restricted
   5.293 +  file-system access only for the current user. The Isabelle/Scala server
   5.294 +  implementation is careful to expose the password only on private output
   5.295 +  channels, and not on a process command-line (which is accessible to other
   5.296 +  users, e.g.\ via the \<^verbatim>\<open>ps\<close> command).
   5.297 +\<close>
   5.298 +
   5.299 +
   5.300 +subsection \<open>Synchronous commands\<close>
   5.301 +
   5.302 +text \<open>
   5.303 +  A \<^emph>\<open>synchronous command\<close> corresponds to regular function application in
   5.304 +  Isabelle/Scala, with single argument and result (regular or error). Both the
   5.305 +  argument and the result may consist of type \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close>.
   5.306 +  An error result typically consists of a JSON object with error message and
   5.307 +  potentially further fields (this resembles exceptions in Scala).
   5.308 +
   5.309 +  These are the protocol exchanges for both cases of command execution:
   5.310 +  \begin{center}
   5.311 +  \begin{tabular}{rl}
   5.312 +  \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   5.313 +  (a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK\<close> \<open>result\<close> \\
   5.314 +  (b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>ERROR\<close> \<open>result\<close> \\
   5.315 +  \end{tabular}
   5.316 +  \end{center}
   5.317 +\<close>
   5.318 +
   5.319 +
   5.320 +subsection \<open>Asynchronous commands\<close>
   5.321 +
   5.322 +text \<open>
   5.323 +  An \<^emph>\<open>asynchronous command\<close> corresponds to an ongoing process that finishes
   5.324 +  or fails eventually, while emitting arbitrary notifications intermediately.
   5.325 +  Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close> and
   5.326 +  the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad command
   5.327 +  syntax. For a running task, the termination is indicated later by
   5.328 +  \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result.
   5.329 +
   5.330 +  These are the protocol exchanges for various cases of command task
   5.331 +  execution:
   5.332 +
   5.333 +  \begin{center}
   5.334 +  \begin{tabular}{rl}
   5.335 +  \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   5.336 +  immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> \\
   5.337 +  intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   5.338 +  intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   5.339 +  (a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
   5.340 +  (b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FAILED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\[3ex]
   5.341 +  \<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
   5.342 +  immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>ERROR\<close>~\<open>\<dots>\<close> \\
   5.343 +  \end{tabular}
   5.344 +  \end{center}
   5.345 +
   5.346 +  All asynchronous messages are decorated with the task identifier that was
   5.347 +  revealed in the immediate (synchronous) result. Thus it is possible to emit
   5.348 +  further asynchronous commands and dispatch the mingled stream of
   5.349 +  asynchronous messages properly.
   5.350 +
   5.351 +  The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
   5.352 +  prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result with error message
   5.353 +  \<^verbatim>\<open>Interrupt\<close>, but this is not guaranteed: the cancel event may come too
   5.354 +  late or the task may just ignore it.
   5.355 +\<close>
   5.356 +
   5.357 +end
     6.1 --- a/src/Doc/System/document/root.tex	Mon Mar 19 18:13:37 2018 +0100
     6.2 +++ b/src/Doc/System/document/root.tex	Mon Mar 19 19:24:45 2018 +0100
     6.3 @@ -33,6 +33,7 @@
     6.4  \input{Environment.tex}
     6.5  \input{Sessions.tex}
     6.6  \input{Presentation.tex}
     6.7 +\input{Server.tex}
     6.8  \input{Scala.tex}
     6.9  \input{Misc.tex}
    6.10  
     7.1 --- a/src/Pure/Tools/server.scala	Mon Mar 19 18:13:37 2018 +0100
     7.2 +++ b/src/Pure/Tools/server.scala	Mon Mar 19 19:24:45 2018 +0100
     7.3 @@ -440,11 +440,11 @@
     7.4    Options are:
     7.5      -L FILE      logging on FILE
     7.6      -c           console interaction with specified server
     7.7 -    -l           list servers (exclusive operation)
     7.8 +    -l           list servers (alternative operation)
     7.9      -n NAME      explicit server name (default: """ + default_name + """)
    7.10      -p PORT      explicit server port
    7.11      -s           assume existing server, no implicit startup
    7.12 -    -x           exit specified server (exclusive operation)
    7.13 +    -x           exit specified server (alternative operation)
    7.14  
    7.15    Manage resident Isabelle servers.
    7.16  """,