1.1 --- a/doc-src/System/basics.tex	Tue May 17 18:10:33 2005 +0200
     1.2 +++ b/doc-src/System/basics.tex	Tue May 17 18:10:34 2005 +0200
     1.3 @@ -391,50 +391,33 @@
     1.4  Isabelle is a generic theorem prover, even w.r.t.\ its user interface.  The
     1.5  \ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
     1.6  uniform way for end-users to invoke a certain interface; which one to start is
     1.7 -determined by the \settdx{ISABELLE_INTERFACE} setting variable.  Also note
     1.8 -that the \texttt{install} utility provides some options to install desktop
     1.9 -environment icons as well (see \S\ref{sec:tool-install}).
    1.10 +determined by the \settdx{ISABELLE_INTERFACE} setting variable, which should
    1.11 +give a full path specification to the actual executable.  Also note that the
    1.12 +\texttt{install} utility provides some options to install desktop environment
    1.13 +icons (see \S\ref{sec:tool-install}).
    1.14  
    1.15 -An interface may be specified either by giving an identifier that the Isabelle
    1.16 -distribution knows about, or by specifying an actual path name (containing a
    1.17 -slash ``\texttt{/}'') of some executable.  Currently, the following interfaces
    1.18 -are available:
    1.19 -
    1.20 -\begin{itemize}
    1.21 -\item \texttt{none} is just a pass-through to raw \texttt{isabelle}. Thus
    1.22 -  \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.  This is
    1.23 -  the factory default.
    1.24 -
    1.25 -\item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user
    1.26 -    interface!Isamode} for emacs.  Isabelle just provides a wrapper for this,
    1.27 -  the actual Isamode distribution is available elsewhere \cite{isamode}.
    1.28 -  
    1.29 -\item Proof~General~\cite{proofgeneral}\index{user interface!Proof General} is
    1.30 -  an advanced interface for common theorem proving environments.  It has
    1.31 -  become the de-facto standard for Isabelle recently, supporting both the old
    1.32 -  ML top-level of classic Isabelle and the more convenient Isabelle/Isar
    1.33 -  interpreter loop.  The Proof~General distributions includes separate
    1.34 -  interface wrapper scripts (in \texttt{ProofGeneral/isa} and
    1.35 -  \texttt{ProofGeneral/isar}).  The canonical settings for Isabelle/Isar are
    1.36 -  as follows:
    1.37 -  \begin{ttbox}
    1.38 +Presently, the most prominent Isabelle interface is
    1.39 +Proof~General~\cite{proofgeneral}\index{user interface!Proof General}.  There
    1.40 +are separate versions for the raw ML top-level and the proper Isabelle/Isar
    1.41 +interpreter loop.  The Proof~General distribution includes separate interface
    1.42 +wrapper scripts (in \texttt{ProofGeneral/isa} and \texttt{ProofGeneral/isar})
    1.43 +for either of these.  The canonical settings for Isabelle/Isar are as follows:
    1.44 +\begin{ttbox}
    1.45  ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
    1.46  PROOFGENERAL_OPTIONS=""
    1.47 -  \end{ttbox}
    1.48 -  Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
    1.49 -  the Proof~General Lisp packages.  There are some options available, such as
    1.50 -  \texttt{-l} for passing the logic image to be used by default, or
    1.51 -  \texttt{-m} to tune the standard print mode.  The \texttt{-I} option allows
    1.52 -  to switch between the Isar and ML view, independently of the interface
    1.53 -  script being used.
    1.54 +\end{ttbox}
    1.55 +Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
    1.56 +the Proof~General Lisp packages.  There are some options available, such as
    1.57 +\texttt{-l} for passing the logic image to be used by default, or \texttt{-m}
    1.58 +to tune the standard print mode.  The \texttt{-I} option allows to switch
    1.59 +between the Isar and ML view, independently of the interface script being
    1.60 +used.
    1.61    
    1.62 -  \medskip Note that the world may be also seen the other way round: Emacs may
    1.63 -  be started first (with proper setup of Proof~General mode), and
    1.64 -  \texttt{isabelle} run from within.  This requires further Emacs Lisp
    1.65 -  configuration, see the Proof~General documentation \cite{proofgeneral} for
    1.66 -  more information.
    1.67 -
    1.68 -\end{itemize}
    1.69 +\medskip Note that the world may be also seen the other way round: Emacs may
    1.70 +be started first (with proper setup of Proof~General mode), and
    1.71 +\texttt{isabelle} run from within.  This requires further Emacs Lisp
    1.72 +configuration, see the Proof~General documentation \cite{proofgeneral} for
    1.73 +more information.
    1.74  
    1.75  %%% Local Variables:
    1.76  %%% mode: latex