doc-src/System/Thy/document/Basics.tex

 
   Options are:
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
-    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
+    -W IN:OUT    startup process wrapper, with input/output fifos
     -X           startup PGIP interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
     -f           pass 'Session.finish();' to the ML session
     -m MODE      add print mode for output
     -q           non-interactive session

 
   \medskip The \verb|-I| option makes Isabelle enter Isar
   interaction mode on startup, instead of the primitive ML top-level.
   The \verb|-P| option configures the top-level loop for
   interaction with the Proof General user interface, and the
-  \verb|-X| option enables XML-based PGIP communication.  The
-  \verb|-W| option makes Isabelle enter a special process
-  wrapper for interaction via an external program; the protocol is a
-  stripped-down version of Proof General the interaction mode, see
-  also \hyperlink{file.~~/src/Pure/System/isabelle-process.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}ML}}}} and \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}.
+  \verb|-X| option enables XML-based PGIP communication.
+
+  \medskip The \verb|-W| option makes Isabelle enter a special
+  process wrapper for interaction via the Isabelle/Scala layer, see
+  also \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}.  The
+  protocol between the ML and JVM process is private to the
+  implementation.
 
   \medskip The \verb|-S| option makes the Isabelle process more
   secure by disabling some critical operations, notably runtime
   compilation and evaluation of ML source code.%
 \end{isamarkuptext}%