33 \isamarkupsection{The Proof General / Emacs interface% |
33 \isamarkupsection{The Proof General / Emacs interface% |
34 } |
34 } |
35 \isamarkuptrue% |
35 \isamarkuptrue% |
36 % |
36 % |
37 \begin{isamarkuptext}% |
37 \begin{isamarkuptext}% |
38 The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs with Proof |
38 The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof |
39 General within the regular Isabelle settings environment |
39 General within the regular Isabelle settings environment |
40 (\secref{sec:settings}). This is more robust than starting Emacs |
40 (\secref{sec:settings}). This is more robust than starting Emacs |
41 separately, loading the Proof General lisp files, and then |
41 separately, loading the Proof General lisp files, and then |
42 attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup |
42 attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup |
43 etc. |
43 etc. |
44 |
44 |
45 The actual interface script is part of the Proof General |
45 The actual interface script is part of the Proof General |
46 distribution~\cite{proofgeneral}; its usage depends on the |
46 distribution~\cite{proofgeneral}; its usage depends on the |
47 particular version. There are some options available, such as |
47 particular version. There are some options available, such as |
48 \verb|-l| for passing the logic image to be used by default, |
48 \verb|-l| for passing the logic image to be used by default, |
49 or \verb|-m| to tune the standard print mode. |
49 or \verb|-m| to tune the standard print mode. The following |
50 |
50 Isabelle settings are particularly important for Proof General: |
51 The following Isabelle settings are particularly important for Proof |
|
52 General: |
|
53 |
51 |
54 \begin{description} |
52 \begin{description} |
55 |
53 |
56 \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main |
54 \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main |
57 installation directory of the Proof General distribution. The |
55 installation directory of the Proof General distribution. The |
61 \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to |
59 \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to |
62 the command line of any invocation of the Proof General \verb|interface| script. |
60 the command line of any invocation of the Proof General \verb|interface| script. |
63 |
61 |
64 \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell |
62 \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell |
65 script to install the X11 fonts required for the X-Symbols mode of |
63 script to install the X11 fonts required for the X-Symbols mode of |
66 Proof General. This is only required if the X11 display server runs |
64 Proof General. This is only relevant if the X11 display server runs |
67 on a different machine than the Emacs application, with a different |
65 on a different machine than the Emacs application, with a different |
68 file-system view on the Proof General installation. Under most |
66 file-system view on the Proof General installation. Under most |
69 circumstances Proof General is able to refer to the font files that |
67 circumstances Proof General is able to refer to the font files that |
70 are part of its distribution. |
68 are part of its distribution. |
71 |
69 |