--- a/src/Doc/System/Misc.thy Tue Mar 08 17:55:11 2016 +0100
+++ b/src/Doc/System/Misc.thy Tue Mar 08 18:15:16 2016 +0100
@@ -72,29 +72,25 @@
-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>}
+ Run Isabelle process with raw ML console and line editor.\<close>}
- The \<^verbatim>\<open>-l\<close> option 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
+ 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>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed directly to @{tool build}
+ 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>, \<^verbatim>\<open>-o\<close> are passed directly to the underlying Isabelle process
- (\secref{sec:isabelle-process}).
+ 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}).
- The Isabelle 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.
-
- Interaction works via the raw ML toplevel loop: this is neither
- Isabelle/Isar nor Isabelle/ML within the usual formal context. Some useful
- ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML use_thys}.
+ \<^medskip>
+ Interaction works via the built-in line editor of Scala, which is based on
+ JLine\<^footnote>\<open>@{url "https://github.com/jline"}\<close>. 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>