equal
deleted
inserted
replaced
367 interaction with the Proof General user interface, and the |
367 interaction with the Proof General user interface, and the |
368 \verb|-X| option enables XML-based PGIP communication. The |
368 \verb|-X| option enables XML-based PGIP communication. The |
369 \verb|-W| option makes Isabelle enter a special process |
369 \verb|-W| option makes Isabelle enter a special process |
370 wrapper for interaction via an external program; the protocol is a |
370 wrapper for interaction via an external program; the protocol is a |
371 stripped-down version of Proof General the interaction mode, see |
371 stripped-down version of Proof General the interaction mode, see |
372 also \hyperlink{file.~~/src/Pure/Tools/isabelle-process.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Tools{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}ML}}}} and \hyperlink{file.~~/src/Pure/Tools/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Tools{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}. |
372 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}}}}. |
373 |
373 |
374 \medskip The \verb|-S| option makes the Isabelle process more |
374 \medskip The \verb|-S| option makes the Isabelle process more |
375 secure by disabling some critical operations, notably runtime |
375 secure by disabling some critical operations, notably runtime |
376 compilation and evaluation of ML source code.% |
376 compilation and evaluation of ML source code.% |
377 \end{isamarkuptext}% |
377 \end{isamarkuptext}% |