--- a/NEWS Tue Sep 16 16:13:31 2008 +0200
+++ b/NEWS Tue Sep 16 17:16:25 2008 +0200
@@ -63,10 +63,11 @@
*** HOL ***
-* HOL/Main: command "value" now integrates different evaluation mechanisms.
-The result of the first successful evaluation mechanism is printed.
-In square brackets a particular named evaluation mechanisms may be specified
-(currently, [SML], [code] or [nbe]). See further HOL/ex/Eval_Examples.thy.
+* HOL/Main: command "value" now integrates different evaluation
+mechanisms. The result of the first successful evaluation mechanism
+is printed. In square brackets a particular named evaluation
+mechanisms may be specified (currently, [SML], [code] or [nbe]). See
+further src/HOL/ex/Eval_Examples.thy.
* HOL/Orderings: class "wellorder" moved here, with explicit induction
rule "less_induct" as assumption. For instantiation of "wellorder" by
@@ -130,8 +131,8 @@
(instead of Main), thus theory Main occasionally has to be imported
explicitly.
-* The metis method now fails in the usual manner, rather than raising an exception,
-if it determines that it cannot prove the theorem.
+* The metis method now fails in the usual manner, rather than raising
+an exception, if it determines that it cannot prove the theorem.
* Methods "case_tac" and "induct_tac" now refer to the very same rules
as the structured Isar versions "cases" and "induct", cf. the
@@ -251,6 +252,12 @@
*** System ***
+* The Isabelle "emacs" tool provides a specific interface to invoke
+Proof General / Emacs, with more explicit failure if that is not
+installed (the old isabelle-interface script silently falls back on
+isabelle-process). The PROOFGENERAL_HOME setting determines the
+installation location of the Proof General distribution.
+
* Isabelle/lib/classes/Pure.jar provides basic support to integrate
the Isabelle process into a JVM/Scala application. See
Isabelle/lib/jedit/plugin for a minimal example. (The obsolete Java
--- a/doc-src/System/Thy/Misc.thy Tue Sep 16 16:13:31 2008 +0200
+++ b/doc-src/System/Thy/Misc.thy Tue Sep 16 17:16:25 2008 +0200
@@ -12,6 +12,48 @@
*}
+section {* The Proof General / Emacs interface *}
+
+text {*
+ The @{tool_def 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 @{setting 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
+ @{verbatim "-l"} for passing the logic image to be used by default,
+ or @{verbatim "-m"} to tune the standard print mode.
+
+ The following Isabelle settings are particularly important for Proof
+ General:
+
+ \begin{description}
+
+ \item[@{setting_def PROOFGENERAL_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 @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}.
+
+ \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
+ the command line of any invocation of the Proof General @{verbatim
+ interface} script.
+
+ \item[@{setting_def XSYMBOL_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}
+*}
+
+
section {* Displaying documents *}
text {*
--- 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%