diff -r d68b74435605 -r af0f5560ac94 doc-src/System/Thy/Interfaces.thy
--- a/doc-src/System/Thy/Interfaces.thy	Sat Jul 28 07:26:37 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy	Sat Jul 28 12:59:53 2012 +0200
@@ -10,14 +10,14 @@
   The @{tool_def tty} tool runs the Isabelle process interactively
   within a plain terminal session:
 \begin{ttbox}
-Usage: tty [OPTIONS]
+Usage: isabelle tty [OPTIONS]
 
   Options are:
     -l NAME      logic image name (default ISABELLE_LOGIC)
     -m MODE      add print mode for output
     -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
 
-  Run Isabelle process with plain tty interaction, and optional line editor.
+  Run Isabelle process with plain tty interaction and line editor.
 \end{ttbox}
 
   The @{verbatim "-l"} option specifies the logic image.  The
@@ -27,39 +27,40 @@
   fall-back is to use raw standard input.
 
   Regular interaction is via the standard Isabelle/Isar toplevel loop.
-  The Isar command @{command exit} drops out into the raw ML system,
-  which is occasionally useful for low-level debugging.  Invoking @{ML
-  Isar.loop}~@{verbatim "();"} in ML will return to the Isar toplevel.
-*}
+  The Isar command @{command exit} drops out into the bare-bones ML
+  system, which is occasionally useful for debugging of the Isar
+  infrastructure itself.  Invoking @{ML Isar.loop}~@{verbatim "();"}
+  in ML will return to the Isar toplevel.  *}
 
 
 section {* Proof General / Emacs *}
 
-text {*
-  The @{tool_def emacs} tool invokes a version of Emacs and Proof
-  General within the regular Isabelle settings environment
-  (\secref{sec:settings}).  This is more robust than starting Emacs
-  separately, loading the Proof General lisp files, and then
-  attempting to start Isabelle with dynamic @{setting PATH} lookup
-  etc.
+text {* The @{tool_def emacs} tool invokes a version of Emacs and
+  Proof General \cite{proofgeneral} within the regular Isabelle
+  settings environment (\secref{sec:settings}).  This is more
+  convenient than starting Emacs separately, loading the Proof General
+  lisp files, and then attempting to start Isabelle with dynamic
+  @{setting PATH} lookup etc.
 
   The actual interface script is part of the Proof General
-  distribution~\cite{proofgeneral}; its usage depends on the
-  particular version.  There are some options available, such as
-  @{verbatim "-l"} for passing the logic image to be used by default,
-  or @{verbatim "-m"} to tune the standard print mode.  The following
-  Isabelle settings are particularly important for Proof General:
+  distribution; its usage depends on the particular version.  There
+  are some options available, such as @{verbatim "-l"} for passing the
+  logic image to be used by default, or @{verbatim "-m"} to tune the
+  standard print mode.  The following Isabelle settings are
+  particularly important for Proof General:
 
   \begin{description}
 
   \item[@{setting_def PROOFGENERAL_HOME}] points to the main
-  installation directory of the Proof General distribution.  The
-  default settings try to locate this in a number of standard places,
-  notably @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}.
+  installation directory of the Proof General distribution.  This is
+  implicitly provided for versions of Proof General that are
+  distributed as Isabelle component, see also \secref{sec:components};
+  otherwise it needs to be configured manually.
 
   \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
   the command line of any invocation of the Proof General @{verbatim
-  interface} script.
+  interface} script.  This allows to provide persistent default
+  options for the invocation of \texttt{isabelle emacs}.
 
   \end{description}
 *}