--- a/src/Doc/System/Misc.thy Thu Mar 10 12:11:23 2016 +0100
+++ b/src/Doc/System/Misc.thy Thu Mar 10 12:11:50 2016 +0100
@@ -56,49 +56,6 @@
\<close>
-section \<open>Raw ML console\<close>
-
-text \<open>
- The @{tool_def console} tool runs the Isabelle process with raw ML console:
- @{verbatim [display]
-\<open>Usage: isabelle console [OPTIONS]
-
- Options are:
- -d DIR include session directory
- -l NAME logic session name (default ISABELLE_LOGIC)
- -m MODE add print mode for output
- -n no build of session image on startup
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r logic session is RAW_ML_SYSTEM
- -s system build mode for session image
-
- Run Isabelle process with raw ML console and line editor
- (default ISABELLE_LINE_EDITOR).\<close>}
-
- Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
- checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
- abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
- Isabelle/Pure interactively.
-
- Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
- (\secref{sec:tool-build}).
-
- Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for the raw @{executable
- isabelle_process} (\secref{sec:isabelle-process}).
-
- \<^medskip>
- The Isabelle/ML process is run through the line editor that is specified via
- the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
- @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
- standard input/output.
-
- The user is connected to the raw ML toplevel loop: this is neither
- Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
- relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
- use_thys}.
-\<close>
-
-
section \<open>Displaying documents \label{sec:tool-display}\<close>
text \<open>
@@ -213,7 +170,7 @@
determined by @{setting ISABELLE_HOME}.
The \<open>BINDIR\<close> argument tells where executable wrapper scripts for
- @{executable "isabelle_process"} and @{executable isabelle} should be
+ @{executable "isabelle"} and @{executable isabelle_scala_script} should be
placed, which is typically a directory in the shell's @{setting PATH}, such
as \<^verbatim>\<open>$HOME/bin\<close>.