diff -r 5ed9bd1d5664 -r 87d095351f8e src/Doc/System/Server.thy --- a/src/Doc/System/Server.thy Sat Nov 08 17:29:57 2025 +0100 +++ b/src/Doc/System/Server.thy Sat Nov 08 20:06:42 2025 +0100 @@ -11,7 +11,7 @@ heavy: Isabelle/Scala for the system infrastructure and Isabelle/ML for the logic session (e.g.\ HOL). In principle, these processes can be invoked directly on the command-line, e.g.\ via @{tool java}, @{tool scala}, @{tool - process}, @{tool console}, but this approach is inadequate for reactive + ML_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 @@ -806,7 +806,7 @@ The \print_mode\ field adds identifiers of print modes to be made active for this session. For example, \<^verbatim>\"print_mode": ["ASCII"]\ prefers ASCII replacement syntax over mathematical Isabelle symbols. See also option \<^verbatim>\-m\ - in @{tool process} (\secref{sec:tool-process}). + in @{tool ML_process} (\secref{sec:tool-ml-process}). \