1.1 --- a/doc-src/System/Thy/document/Misc.tex	Sun Nov 30 14:03:45 2008 +0100
     1.2 +++ b/doc-src/System/Thy/document/Misc.tex	Sun Nov 30 14:03:46 2008 +0100
     1.3 @@ -30,47 +30,6 @@
     1.4  \end{isamarkuptext}%
     1.5  \isamarkuptrue%
     1.6  %
     1.7 -\isamarkupsection{The Proof General / Emacs interface%
     1.8 -}
     1.9 -\isamarkuptrue%
    1.10 -%
    1.11 -\begin{isamarkuptext}%
    1.12 -The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof
    1.13 -  General within the regular Isabelle settings environment
    1.14 -  (\secref{sec:settings}).  This is more robust than starting Emacs
    1.15 -  separately, loading the Proof General lisp files, and then
    1.16 -  attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup
    1.17 -  etc.
    1.18 -
    1.19 -  The actual interface script is part of the Proof General
    1.20 -  distribution~\cite{proofgeneral}; its usage depends on the
    1.21 -  particular version.  There are some options available, such as
    1.22 -  \verb|-l| for passing the logic image to be used by default,
    1.23 -  or \verb|-m| to tune the standard print mode.  The following
    1.24 -  Isabelle settings are particularly important for Proof General:
    1.25 -
    1.26 -  \begin{description}
    1.27 -
    1.28 -  \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main
    1.29 -  installation directory of the Proof General distribution.  The
    1.30 -  default settings try to locate this in a number of standard places,
    1.31 -  notably \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
    1.32 -
    1.33 -  \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to
    1.34 -  the command line of any invocation of the Proof General \verb|interface| script.
    1.35 -
    1.36 -  \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell
    1.37 -  script to install the X11 fonts required for the X-Symbols mode of
    1.38 -  Proof General.  This is only relevant if the X11 display server runs
    1.39 -  on a different machine than the Emacs application, with a different
    1.40 -  file-system view on the Proof General installation.  Under most
    1.41 -  circumstances Proof General is able to refer to the font files that
    1.42 -  are part of its distribution.
    1.43 -
    1.44 -  \end{description}%
    1.45 -\end{isamarkuptext}%
    1.46 -\isamarkuptrue%
    1.47 -%
    1.48  \isamarkupsection{Displaying documents%
    1.49  }
    1.50  \isamarkuptrue%
    1.51 @@ -329,32 +288,6 @@
    1.52  \end{isamarkuptext}%
    1.53  \isamarkuptrue%
    1.54  %
    1.55 -\isamarkupsection{Run Isabelle with plain tty interaction \label{sec:tool-tty}%
    1.56 -}
    1.57 -\isamarkuptrue%
    1.58 -%
    1.59 -\begin{isamarkuptext}%
    1.60 -The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} utility runs the Isabelle process interactively
    1.61 -  within a plain terminal session:
    1.62 -\begin{ttbox}
    1.63 -Usage: tty [OPTIONS]
    1.64 -
    1.65 -  Options are:
    1.66 -    -l NAME      logic image name (default ISABELLE_LOGIC)
    1.67 -    -m MODE      add print mode for output
    1.68 -    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
    1.69 -
    1.70 -  Run Isabelle process with plain tty interaction, and optional line editor.
    1.71 -\end{ttbox}
    1.72 -
    1.73 -  The \verb|-l| option specifies the logic image.  The
    1.74 -  \verb|-m| option specifies additional print modes.  The The
    1.75 -  \verb|-p| option specifies an alternative line editor (such
    1.76 -  as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
    1.77 -  fall-back is to use raw standard input.%
    1.78 -\end{isamarkuptext}%
    1.79 -\isamarkuptrue%
    1.80 -%
    1.81  \isamarkupsection{Remove awkward symbol names from theory sources%
    1.82  }
    1.83  \isamarkuptrue%