diff -r c46418f12ee1 -r 83e815849a91 src/Doc/System/Misc.thy
--- 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>