|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Interfaces}% |
|
4 % |
|
5 \isadelimtheory |
|
6 \isanewline |
|
7 \isanewline |
|
8 % |
|
9 \endisadelimtheory |
|
10 % |
|
11 \isatagtheory |
|
12 \isacommand{theory}\isamarkupfalse% |
|
13 \ Interfaces\isanewline |
|
14 \isakeyword{imports}\ Pure\isanewline |
|
15 \isakeyword{begin}% |
|
16 \endisatagtheory |
|
17 {\isafoldtheory}% |
|
18 % |
|
19 \isadelimtheory |
|
20 % |
|
21 \endisadelimtheory |
|
22 % |
|
23 \isamarkupchapter{User interfaces% |
|
24 } |
|
25 \isamarkuptrue% |
|
26 % |
|
27 \isamarkupsection{Plain TTY interaction \label{sec:tool-tty}% |
|
28 } |
|
29 \isamarkuptrue% |
|
30 % |
|
31 \begin{isamarkuptext}% |
|
32 The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively |
|
33 within a plain terminal session: |
|
34 \begin{ttbox} |
|
35 Usage: tty [OPTIONS] |
|
36 |
|
37 Options are: |
|
38 -l NAME logic image name (default ISABELLE_LOGIC) |
|
39 -m MODE add print mode for output |
|
40 -p NAME line editor program name (default ISABELLE_LINE_EDITOR) |
|
41 |
|
42 Run Isabelle process with plain tty interaction, and optional line editor. |
|
43 \end{ttbox} |
|
44 |
|
45 The \verb|-l| option specifies the logic image. The |
|
46 \verb|-m| option specifies additional print modes. The The |
|
47 \verb|-p| option specifies an alternative line editor (such |
|
48 as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the |
|
49 fall-back is to use raw standard input. |
|
50 |
|
51 Regular interaction is via the standard Isabelle/Isar toplevel loop. |
|
52 The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the raw ML system, |
|
53 which is occasionally useful for low-level debugging. Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.% |
|
54 \end{isamarkuptext}% |
|
55 \isamarkuptrue% |
|
56 % |
|
57 \isamarkupsection{Proof General / Emacs% |
|
58 } |
|
59 \isamarkuptrue% |
|
60 % |
|
61 \begin{isamarkuptext}% |
|
62 The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof |
|
63 General within the regular Isabelle settings environment |
|
64 (\secref{sec:settings}). This is more robust than starting Emacs |
|
65 separately, loading the Proof General lisp files, and then |
|
66 attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup |
|
67 etc. |
|
68 |
|
69 The actual interface script is part of the Proof General |
|
70 distribution~\cite{proofgeneral}; its usage depends on the |
|
71 particular version. There are some options available, such as |
|
72 \verb|-l| for passing the logic image to be used by default, |
|
73 or \verb|-m| to tune the standard print mode. The following |
|
74 Isabelle settings are particularly important for Proof General: |
|
75 |
|
76 \begin{description} |
|
77 |
|
78 \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main |
|
79 installation directory of the Proof General distribution. The |
|
80 default settings try to locate this in a number of standard places, |
|
81 notably \verb|$ISABELLE_HOME/contrib/ProofGeneral|. |
|
82 |
|
83 \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to |
|
84 the command line of any invocation of the Proof General \verb|interface| script. |
|
85 |
|
86 \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell |
|
87 script to install the X11 fonts required for the X-Symbols mode of |
|
88 Proof General. This is only relevant if the X11 display server runs |
|
89 on a different machine than the Emacs application, with a different |
|
90 file-system view on the Proof General installation. Under most |
|
91 circumstances Proof General is able to refer to the font files that |
|
92 are part of its distribution. |
|
93 |
|
94 \end{description}% |
|
95 \end{isamarkuptext}% |
|
96 \isamarkuptrue% |
|
97 % |
|
98 \isadelimtheory |
|
99 % |
|
100 \endisadelimtheory |
|
101 % |
|
102 \isatagtheory |
|
103 \isacommand{end}\isamarkupfalse% |
|
104 % |
|
105 \endisatagtheory |
|
106 {\isafoldtheory}% |
|
107 % |
|
108 \isadelimtheory |
|
109 % |
|
110 \endisadelimtheory |
|
111 \end{isabellebody}% |
|
112 %%% Local Variables: |
|
113 %%% mode: latex |
|
114 %%% TeX-master: "root" |
|
115 %%% End: |