src/Doc/System/Server.thy

   process}, @{tool console}, but this approach is inadequate for reactive
   applications that require quick responses from the prover.
 
   In contrast, the Isabelle server exposes Isabelle/Scala as a
   ``terminate-stay-resident'' application that manages multiple logic
-  \<^emph>\<open>sessions\<close> and concurrent tasks to use \<^emph>\<open>theories\<close>. This provides an
-  analogous to \<^ML>\<open>Thy_Info.use_theories\<close> in Isabelle/ML, but with full
-  concurrency and Isabelle/PIDE markup.
+  \<^emph>\<open>sessions\<close> and concurrent tasks to use \<^emph>\<open>theories\<close>. This is analogous to
+  \<^ML>\<open>Thy_Info.use_theories\<close> in Isabelle/ML, with proper support for
+  concurrent invocations.
 
   The client/server arrangement via TCP sockets also opens possibilities for
   remote Isabelle services that are accessed by local applications, e.g.\ via
   an SSH tunnel.
 \<close>

 
     \<^item> A \<^emph>\<open>short message\<close> consists of a single line: it is a sequence of
     arbitrary bytes excluding CR (13) and LF (10), and terminated by CR-LF or
     just LF.
 
-    \<^item> A \<^emph>\<open>long message\<close> starts with a single that consists only of decimal
+    \<^item> A \<^emph>\<open>long message\<close> starts with a single line consisting of decimal
     digits: these are interpreted as length of the subsequent block of
     arbitrary bytes. A final line-terminator (as above) may be included here,
     but is not required.
 
   Messages in JSON format (see below) always fit on a single line, due to

 
 
 subsection \<open>Input and output messages \label{sec:input-output-messages}\<close>
 
 text \<open>
-  Server input and output messages have a uniform format as follows:
-
-    \<^item> \<open>name argument\<close> such that:
+  The uniform format for server input and output messages is \<open>name argument\<close>,
+  such that:
 
     \<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
     ``\<^verbatim>\<open>_\<close>'', ``\<^verbatim>\<open>.\<close>'',
 
     \<^item> the separator between \<open>name\<close> and \<open>argument\<close> is the longest possible

     \<^item> empty argument (Scala type \<^verbatim>\<open>Unit\<close>)
     \<^item> XML element in YXML notation (Scala type \<^verbatim>\<open>XML.Elem\<close>)
     \<^item> JSON value (Scala type \<^verbatim>\<open>JSON.T\<close>)
 
   JSON values may consist of objects (records), arrays (lists), strings,
-  numbers, bools, null.\<^footnote>\<open>See also the official specification
+  numbers, bools, or null.\<^footnote>\<open>See also the official specification
   \<^url>\<open>https://www.json.org\<close> and unofficial explorations ``Parsing JSON is a
   Minefield'' \<^url>\<open>http://seriot.ch/parsing_json.php\<close>.\<close> Since JSON requires
   explicit quotes and backslash-escapes to represent arbitrary text, the YXML
   notation for XML trees (\secref{sec:yxml-vs-xml}) works better
   for large messages with a lot of PIDE markup.

 
 subsubsection \<open>Results\<close>
 
 text \<open>
   The \<open>session_id\<close> provides the internal identification of the session object
-  within the sever process. It can remain active as long as the server is
+  within the server process. It can remain active as long as the server is
   running, independently of the current client connection.
 
   \<^medskip>
   The \<open>tmp_dir\<close> field refers to a temporary directory that is specifically
   created for this session and deleted after it has been stopped. This may