1.1 --- a/doc-src/System/Thy/Basics.thy	Sun Nov 30 14:03:45 2008 +0100
     1.2 +++ b/doc-src/System/Thy/Basics.thy	Sun Nov 30 14:03:46 2008 +0100
     1.3 @@ -8,19 +8,18 @@
     1.4  
     1.5  text {*
     1.6    This manual describes Isabelle together with related tools and user
     1.7 -  interfaces as seen from an outside (system oriented) view.  See also
     1.8 -  the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
     1.9 -  and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
    1.10 -  actual Isabelle commands and related functions.
    1.11 +  interfaces as seen from a system oriented view.  See also the
    1.12 +  \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
    1.13 +  the actual Isabelle input language and related concepts.
    1.14  
    1.15 -  \medskip The Isabelle system environment emerges from a few general
    1.16 -  concepts.
    1.17 +  \medskip The Isabelle system environment provides the following
    1.18 +  basic infrastructure to integrate tools smoothly.
    1.19  
    1.20    \begin{enumerate}
    1.21  
    1.22 -  \item The \emph{Isabelle settings} mechanism provides environment
    1.23 -  variables to all Isabelle programs (including tools and user
    1.24 -  interfaces).
    1.25 +  \item The \emph{Isabelle settings} mechanism provides process
    1.26 +  environment variables to all Isabelle executables (including tools
    1.27 +  and user interfaces).
    1.28  
    1.29    \item The \emph{raw Isabelle process} (@{executable_ref
    1.30    "isabelle-process"}) runs logic sessions either interactively or in
    1.31 @@ -33,11 +32,6 @@
    1.32    user interfaces etc.  Such tools automatically benefit from the
    1.33    settings mechanism.
    1.34  
    1.35 -  \item The \emph{Isabelle interface wrapper} (@{executable_ref
    1.36 -  "isabelle-interface"}) provides some abstraction over the actual
    1.37 -  user interface to be used.  The de-facto standard interface for
    1.38 -  Isabelle is Proof~General \cite{proofgeneral}.
    1.39 -
    1.40    \end{enumerate}
    1.41  *}
    1.42  
    1.43 @@ -256,11 +250,6 @@
    1.44    derives an individual directory for temporary files.  The default is
    1.45    somewhere in @{verbatim "/tmp"}.
    1.46    
    1.47 -  \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that
    1.48 -  specifies the actual user interface that the capital @{executable
    1.49 -  Isabelle} or @{executable "isabelle-interface"} should invoke.  See
    1.50 -  \secref{sec:interface} for more details.
    1.51 -
    1.52    \end{description}
    1.53  *}
    1.54  
    1.55 @@ -480,41 +469,4 @@
    1.56    by @{verbatim "isabelle make"} alone.
    1.57  *}
    1.58  
    1.59 -
    1.60 -section {* The Isabelle interface wrapper \label{sec:interface} *}
    1.61 -
    1.62 -text {*
    1.63 -  Isabelle is a generic theorem prover, even w.r.t.\ its user
    1.64 -  interface.  The @{executable_def Isabelle} (or @{executable_def
    1.65 -  "isabelle-interface"}) executable provides a uniform way for
    1.66 -  end-users to invoke a certain interface; which one to start is
    1.67 -  determined by the @{setting_ref ISABELLE_INTERFACE} setting
    1.68 -  variable, which should give a full path specification to the actual
    1.69 -  executable.
    1.70 -
    1.71 -  Presently, the most prominent Isabelle interface is Proof
    1.72 -  General~\cite{proofgeneral}\index{user interface!Proof General}.
    1.73 -  The Proof General distribution includes an interface wrapper script
    1.74 -  for the regular Isar toplevel, see @{verbatim
    1.75 -  "ProofGeneral/isar/interface"}.  The canonical settings for
    1.76 -  Isabelle/Isar are as follows:
    1.77 -
    1.78 -\begin{ttbox}
    1.79 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
    1.80 -PROOFGENERAL_OPTIONS=""
    1.81 -\end{ttbox}
    1.82 -
    1.83 -  Thus @{executable Isabelle} would automatically invoke Emacs with
    1.84 -  proper setup of the Proof General Lisp packages.  There are some
    1.85 -  options available, such as @{verbatim "-l"} for passing the logic
    1.86 -  image to be used by default, or @{verbatim "-m"} to tune the
    1.87 -  standard print mode.
    1.88 -  
    1.89 -  \medskip Note that the world may be also seen the other way round:
    1.90 -  Emacs may be started first (with proper setup of Proof General
    1.91 -  mode), and @{executable "isabelle-process"} run from within.  This
    1.92 -  requires further Emacs Lisp configuration, see the Proof General
    1.93 -  documentation \cite{proofgeneral} for more information.
    1.94 -*}
    1.95 -
    1.96  end
    1.97 \ No newline at end of file