src/Doc/System/Server.thy

   \medskip Subsequently, the protocol message formats are described in further
   detail.
 \<close>
 
 
-subsection \<open>Byte messages\<close>
+subsection \<open>Byte messages \label{sec:byte-messages}\<close>
 
 text \<open>
   The client-server connection is a raw byte-channel for bidirectional
   communication, but the Isabelle server always works with messages of a
   particular length. Messages are written as a single chunk that is flushed

 
 subsection \<open>Initial password exchange\<close>
 
 text \<open>
   Whenever a new client opens the server socket, the initial message needs to
-  be its unique password. The server replies either with \<^verbatim>\<open>OK\<close> (and some
-  information about the Isabelle version) or by silent disconnection of what
-  is considered an illegal connection attempt. Note that @{tool client}
-  already presents the correct password internally.
+  be its unique password as a single line, without length indication (i.e.\ a
+  ``short message'' in the sense of \secref{sec:byte-messages}).
+
+  The server replies either with \<^verbatim>\<open>OK\<close> (and some information about the
+  Isabelle version) or by silent disconnection of what is considered an
+  illegal connection attempt. Note that @{tool client} already presents the
+  correct password internally.
 
   Server passwords are created as Universally Unique Identifier (UUID) in
   Isabelle/Scala and stored in a per-user database, with restricted
   file-system access only for the current user. The Isabelle/Scala server
   implementation is careful to expose the password only on private output