# HG changeset patch
# User wenzelm
# Date 936375362 -7200
# Node ID b1b2fbc375e216978b2d70e75ef2da8d4e7d850d
# Parent  173efad74891b2c846d5bdf94c0203d86d16e651
tuned;

diff -r 173efad74891 -r b1b2fbc375e2 doc-src/IsarRef/intro.tex
--- a/doc-src/IsarRef/intro.tex	Fri Sep 03 17:52:13 1999 +0200
+++ b/doc-src/IsarRef/intro.tex	Fri Sep 03 18:16:02 1999 +0200
@@ -44,22 +44,22 @@
 \begin{ttbox}
 Usage: interface [OPTIONS] [FILES ...]
 
-Options are:
-  -l NAME      logic image name (default $ISABELLE_LOGIC=HOL)
-  -p NAME      Emacs program name (default xemacs)
-  -u BOOL      use .emacs file (default false)
-  -w BOOL      use window system (default true)
+  Options are:
+    -l NAME      logic image name (default $ISABELLE_LOGIC=HOL)
+    -p NAME      Emacs program name (default xemacs)
+    -u BOOL      use .emacs file (default true)
+    -w BOOL      use window system (default true)
 
-Starts Proof General for Isabelle/Isar with proof documents FILES
-(default Scratch.thy).
+  Starts Proof General for Isabelle/Isar with proof documents FILES
+  (default Scratch.thy).
+
+  PROOFGENERAL_OPTIONS=
 \end{ttbox}
 Apart from the command line, the defaults for these options may be overridden
 via the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For example, plain GNU
-Emacs with loading of the startup file enabled\footnote{The interface disables
-  \texttt{.emacs} by default to ensure successful startup despite any strange
-  commands that tend to occur there.} may be configured as follows:
+Emacs may be configured as follows:
 \begin{ttbox}
-PROOFGENERAL_OPTIONS="-p emacs -u true"
+PROOFGENERAL_OPTIONS="-p emacs"
 \end{ttbox}
 
 With the proper Isabelle interface setup, Isar documents may now be edited by
@@ -71,6 +71,16 @@
 through the text.  Consult the Proof~General documentation \cite{proofgeneral}
 for further basic commands, such as \texttt{c-c return} or \texttt{c-c u}.
 
+\medskip
+
+Occasionally, a user's \texttt{.emacs} contains material that is incompatible
+with the version of (X)Emacs that Proof~General prefers.  Then proper startup
+may be still achieved by using the \texttt{-u false} option.\footnote{Also
+  note that the Emacs lisp files
+  \texttt{\$ISABELLE_HOME/etc/proofgeneral-settings.el} and
+  \texttt{\$ISABELLE_HOME_USER/etc/proofgeneral-settings.el} are automatically
+  loaded by Proof~General if invoked via the interface wrapper script.}
+
 
 \section{How to write Isar proofs anyway?}