diff -r 663037c5d848 -r 0e41f26a0250 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Mon Jun 30 09:31:32 2014 +0200
+++ b/src/Doc/System/Basics.thy	Mon Jun 30 09:43:44 2014 +0200
@@ -249,8 +249,8 @@
   load if none is given explicitely by the user.  The default value is
   @{verbatim HOL}.
   
-  \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
-  line editor for the @{tool_ref tty} interface.
+  \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the
+  line editor for the @{tool_ref console} interface.
 
   \item[@{setting_def ISABELLE_LATEX}, @{setting_def
   ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX}
@@ -350,7 +350,7 @@
 *}
 
 
-section {* The raw Isabelle process *}
+section {* The raw Isabelle process \label{sec:isabelle-process} *}
 
 text {*
   The @{executable_def "isabelle_process"} executable runs bare-bones