# HG changeset patch # User wenzelm # Date 1221578185 -7200 # Node ID b2869ebcf8e3f9fc76fc48aa8bca0d5c7e1cea65 # Parent 8aa636a9e2ce18cb54c04ce6cbdc8a2e58ef9717 separate emacs tool for Proof General / Emacs; diff -r 8aa636a9e2ce -r b2869ebcf8e3 NEWS --- 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 diff -r 8aa636a9e2ce -r b2869ebcf8e3 doc-src/System/Thy/Misc.thy --- 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 {* diff -r 8aa636a9e2ce -r b2869ebcf8e3 doc-src/System/Thy/document/Misc.tex --- 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%