--- a/doc-src/System/Thy/document/Misc.tex Tue Sep 16 16:13:31 2008 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Tue Sep 16 17:16:25 2008 +0200
@@ -30,6 +30,49 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{The Proof General / Emacs interface%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs with 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 \hyperlink{setting.PATH}{\mbox{\isa{\isatt{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
+ \verb|-l| for passing the logic image to be used by default,
+ or \verb|-m| to tune the standard print mode.
+
+ The following Isabelle settings are particularly important for Proof
+ General:
+
+ \begin{description}
+
+ \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}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 \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
+
+ \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to
+ the command line of any invocation of the Proof General \verb|interface| script.
+
+ \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell
+ script to install the X11 fonts required for the X-Symbols mode of
+ Proof General. This is only required if the X11 display server runs
+ on a different machine than the Emacs application, with a different
+ file-system view on the Proof General installation. Under most
+ circumstances Proof General is able to refer to the font files that
+ are part of its distribution.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Displaying documents%
}
\isamarkuptrue%