src/Doc/System/Basics.thy

--- a/src/Doc/System/Basics.thy	Wed Mar 09 16:53:14 2016 +0100
+++ b/src/Doc/System/Basics.thy	Wed Mar 09 19:30:09 2016 +0100
@@ -22,9 +22,7 @@
   to all Isabelle executables (including tools and user interfaces).
 
   \<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref "isabelle_process"}) runs
-  logic sessions either interactively or in batch mode. In particular, this
-  view abstracts over the invocation of the actual ML system to be used.
-  Regular users rarely need to care about the low-level process.
+  logic sessions in batch mode. This is rarely required for regular users.
 
   \<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref isabelle}) provides a
   generic startup environment Isabelle related utilities, user interfaces etc.
@@ -289,35 +287,25 @@
 section \<open>The raw Isabelle process \label{sec:isabelle-process}\<close>
 
 text \<open>
-  The @{executable_def "isabelle_process"} executable runs bare-bones Isabelle
-  logic sessions --- either interactively or in batch mode. It provides an
-  abstraction over the underlying ML system and its saved heap files. Its
-  usage is:
+  The @{executable_def "isabelle_process"} executable runs a bare-bone
+  Isabelle logic session in batch mode:
   @{verbatim [display]
 \<open>Usage: isabelle_process [OPTIONS] [HEAP]
 
   Options are:
-    -O           system options from given YXML file
-    -P SOCKET    startup process wrapper via TCP socket
-    -S           secure mode -- disallow critical operations
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
     -m MODE      add print mode for output
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
-    -q           non-interactive session
 
-  If HEAP is a plain name (default "HOL"), it is searched in $ISABELLE_PATH;
-  if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM,
-  the initial ML heap is used.\<close>}
+  If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
+  $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
+  if it is RAW_ML_SYSTEM, the initial ML heap is used.\<close>}
 
-  Heap files without path specifications are looked up in the @{setting
-  ISABELLE_PATH} setting, which may consist of multiple components separated
-  by colons --- these are tried in the given order with the value of @{setting
-  ML_IDENTIFIER} appended internally. In a similar way, base names are
-  relative to the directory specified by @{setting ISABELLE_OUTPUT}. In any
-  case, actual file locations may also be given by including at least one
-  slash (\<^verbatim>\<open>/\<close>) in the name (hint: use \<^verbatim>\<open>./\<close> to refer to the current
-  directory).
+  Heap files without explicit directory specifications are looked up in the
+  @{setting ISABELLE_PATH} setting, which may consist of multiple components
+  separated by colons --- these are tried in the given order with the value of
+  @{setting ML_IDENTIFIER} appended internally.
 \<close>
 
 
@@ -331,45 +319,22 @@
 
   \<^medskip>
   The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
-  session. Typically, this is used by some user interface, e.g.\ to enable
-  output of proper mathematical symbols.
-
-  \<^medskip>
-  Isabelle normally enters an interactive top-level loop (after processing the
-  \<^verbatim>\<open>-e\<close> texts). The \<^verbatim>\<open>-q\<close> option inhibits interaction, thus providing a pure
-  batch mode facility.
+  session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
+  mathematical Isabelle symbols.
 
   \<^medskip>
   Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
-  see also \secref{sec:system-options}. Alternatively, option \<^verbatim>\<open>-O\<close> specifies
-  the full environment of system options as a file in YXML format (according
-  to the Isabelle/Scala function \<^verbatim>\<open>isabelle.Options.encode\<close>).
-
-  \<^medskip>
-  The \<^verbatim>\<open>-P\<close> option starts the Isabelle process wrapper for Isabelle/Scala,
-  with a private protocol running over the specified TCP socket. Isabelle/ML
-  and Isabelle/Scala provide various programming interfaces to invoke protocol
-  functions over untyped strings and XML trees.
-
-  \<^medskip>
-  The \<^verbatim>\<open>-S\<close> option makes the Isabelle process more secure by disabling some
-  critical operations, notably runtime compilation and evaluation of ML source
-  code.
+  see also \secref{sec:system-options}.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  Run an interactive session of the default object-logic (as specified by the
-  @{setting ISABELLE_LOGIC} setting) like this:
-  @{verbatim [display] \<open>isabelle_process\<close>}
-
-  \<^medskip>
-  The next example demonstrates batch execution of Isabelle. We retrieve the
-  \<^verbatim>\<open>Main\<close> theory value from the theory loader within ML (observe the delicate
-  quoting rules for the Bash shell vs.\ ML):
-  @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' -q HOL\<close>}
+  In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\<open>Main\<close>
+  theory value from the theory loader within ML (observe the delicate quoting
+  rules for the Bash shell vs.\ ML):
+  @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
 
   Note that the output text will be interspersed with additional junk messages
   by the ML runtime environment.