1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Interfaces}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 \isacommand{theory}\isamarkupfalse% |
|
11 \ Interfaces\isanewline |
|
12 \isakeyword{imports}\ Base\isanewline |
|
13 \isakeyword{begin}% |
|
14 \endisatagtheory |
|
15 {\isafoldtheory}% |
|
16 % |
|
17 \isadelimtheory |
|
18 % |
|
19 \endisadelimtheory |
|
20 % |
|
21 \isamarkupchapter{User interfaces% |
|
22 } |
|
23 \isamarkuptrue% |
|
24 % |
|
25 \isamarkupsection{Isabelle/jEdit Prover IDE \label{sec:tool-jedit}% |
|
26 } |
|
27 \isamarkuptrue% |
|
28 % |
|
29 \begin{isamarkuptext}% |
|
30 The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatool{jedit}}}}} tool invokes a version of |
|
31 jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented |
|
32 with some components to provide a fully-featured Prover IDE: |
|
33 \begin{ttbox} Usage: isabelle jedit [OPTIONS] |
|
34 [FILES ...] |
|
35 |
|
36 Options are: |
|
37 -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS) |
|
38 -b build only |
|
39 -d DIR include session directory |
|
40 -f fresh build |
|
41 -j OPTION add jEdit runtime option (default JEDIT_OPTIONS) |
|
42 -l NAME logic image name (default ISABELLE_LOGIC) |
|
43 -m MODE add print mode for output |
|
44 |
|
45 Start jEdit with Isabelle plugin setup and opens theory FILES |
|
46 (default Scratch.thy). |
|
47 \end{ttbox} |
|
48 |
|
49 The \verb|-l| option specifies the session name of the logic |
|
50 image to be used for proof processing. Additional session root |
|
51 directories may be included via option \verb|-d| to augment |
|
52 that name space (see also \secref{sec:tool-build}). |
|
53 |
|
54 The \verb|-m| option specifies additional print modes. |
|
55 |
|
56 The \verb|-J| and \verb|-j| options allow to pass |
|
57 additional low-level options to the JVM or jEdit, respectively. The |
|
58 defaults are provided by the Isabelle settings environment |
|
59 (\secref{sec:settings}). |
|
60 |
|
61 The \verb|-b| and \verb|-f| options control the |
|
62 self-build mechanism of Isabelle/jEdit. This is only relevant for |
|
63 building from sources, which also requires an auxiliary \verb|jedit_build| |
|
64 component.\footnote{\url{http://isabelle.in.tum.de/components}} Note |
|
65 that official Isabelle releases already include a version of |
|
66 Isabelle/jEdit that is built properly.% |
|
67 \end{isamarkuptext}% |
|
68 \isamarkuptrue% |
|
69 % |
|
70 \isamarkupsection{Proof General / Emacs% |
|
71 } |
|
72 \isamarkuptrue% |
|
73 % |
|
74 \begin{isamarkuptext}% |
|
75 The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatool{emacs}}}}} tool invokes a version of Emacs and |
|
76 Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the |
|
77 regular Isabelle settings environment (\secref{sec:settings}). This |
|
78 is more convenient than starting Emacs separately, loading the Proof |
|
79 General LISP files, and then attempting to start Isabelle with |
|
80 dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup etc. |
|
81 |
|
82 The actual interface script is part of the Proof General |
|
83 distribution; its usage depends on the particular version. There |
|
84 are some options available, such as \verb|-l| for passing the |
|
85 logic image to be used by default, or \verb|-m| to tune the |
|
86 standard print mode. The following Isabelle settings are |
|
87 particularly important for Proof General: |
|
88 |
|
89 \begin{description} |
|
90 |
|
91 \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}] points to the main |
|
92 installation directory of the Proof General distribution. This is |
|
93 implicitly provided for versions of Proof General that are |
|
94 distributed as Isabelle component, see also \secref{sec:components}; |
|
95 otherwise it needs to be configured manually. |
|
96 |
|
97 \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}}] is implicitly prefixed to |
|
98 the command line of any invocation of the Proof General \verb|interface| script. This allows to provide persistent default |
|
99 options for the invocation of \texttt{isabelle emacs}. |
|
100 |
|
101 \end{description}% |
|
102 \end{isamarkuptext}% |
|
103 \isamarkuptrue% |
|
104 % |
|
105 \isamarkupsection{Plain TTY interaction \label{sec:tool-tty}% |
|
106 } |
|
107 \isamarkuptrue% |
|
108 % |
|
109 \begin{isamarkuptext}% |
|
110 The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatool{tty}}}}} tool runs the Isabelle process interactively |
|
111 within a plain terminal session: |
|
112 \begin{ttbox} |
|
113 Usage: isabelle tty [OPTIONS] |
|
114 |
|
115 Options are: |
|
116 -l NAME logic image name (default ISABELLE_LOGIC) |
|
117 -m MODE add print mode for output |
|
118 -p NAME line editor program name (default ISABELLE_LINE_EDITOR) |
|
119 |
|
120 Run Isabelle process with plain tty interaction and line editor. |
|
121 \end{ttbox} |
|
122 |
|
123 The \verb|-l| option specifies the logic image. The |
|
124 \verb|-m| option specifies additional print modes. The |
|
125 \verb|-p| option specifies an alternative line editor (such |
|
126 as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the |
|
127 fall-back is to use raw standard input. |
|
128 |
|
129 Regular interaction works via the standard Isabelle/Isar toplevel |
|
130 loop. The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the |
|
131 bare-bones ML system, which is occasionally useful for debugging of |
|
132 the Isar infrastructure itself. Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.% |
|
133 \end{isamarkuptext}% |
|
134 \isamarkuptrue% |
|
135 % |
|
136 \isamarkupsection{Theory graph browser \label{sec:browse}% |
|
137 } |
|
138 \isamarkuptrue% |
|
139 % |
|
140 \begin{isamarkuptext}% |
|
141 The Isabelle graph browser is a general tool for visualizing |
|
142 dependency graphs. Certain nodes of the graph (i.e.\ theories) can |
|
143 be grouped together in ``directories'', whose contents may be |
|
144 hidden, thus enabling the user to collapse irrelevant portions of |
|
145 information. The browser is written in Java, it can be used both as |
|
146 a stand-alone application and as an applet.% |
|
147 \end{isamarkuptext}% |
|
148 \isamarkuptrue% |
|
149 % |
|
150 \isamarkupsubsection{Invoking the graph browser% |
|
151 } |
|
152 \isamarkuptrue% |
|
153 % |
|
154 \begin{isamarkuptext}% |
|
155 The stand-alone version of the graph browser is wrapped up as |
|
156 \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatool{browser}}}}}: |
|
157 \begin{ttbox} |
|
158 Usage: isabelle browser [OPTIONS] [GRAPHFILE] |
|
159 |
|
160 Options are: |
|
161 -b Admin/build only |
|
162 -c cleanup -- remove GRAPHFILE after use |
|
163 -o FILE output to FILE (ps, eps, pdf) |
|
164 \end{ttbox} |
|
165 When no filename is specified, the browser automatically changes to |
|
166 the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}. |
|
167 |
|
168 \medskip The \verb|-b| option indicates that this is for |
|
169 administrative build only, i.e.\ no browser popup if no files are |
|
170 given. |
|
171 |
|
172 The \verb|-c| option causes the input file to be removed |
|
173 after use. |
|
174 |
|
175 The \verb|-o| option indicates batch-mode operation, with the |
|
176 output written to the indicated file; note that \verb|pdf| |
|
177 produces an \verb|eps| copy as well. |
|
178 |
|
179 \medskip The applet version of the browser is part of the standard |
|
180 WWW theory presentation, see the link ``theory dependencies'' within |
|
181 each session index.% |
|
182 \end{isamarkuptext}% |
|
183 \isamarkuptrue% |
|
184 % |
|
185 \isamarkupsubsection{Using the graph browser% |
|
186 } |
|
187 \isamarkuptrue% |
|
188 % |
|
189 \begin{isamarkuptext}% |
|
190 The browser's main window, which is shown in |
|
191 \figref{fig:browserwindow}, consists of two sub-windows. In the |
|
192 left sub-window, the directory tree is displayed. The graph itself |
|
193 is displayed in the right sub-window. |
|
194 |
|
195 \begin{figure}[ht] |
|
196 \includegraphics[width=\textwidth]{browser_screenshot} |
|
197 \caption{\label{fig:browserwindow} Browser main window} |
|
198 \end{figure}% |
|
199 \end{isamarkuptext}% |
|
200 \isamarkuptrue% |
|
201 % |
|
202 \isamarkupsubsubsection{The directory tree window% |
|
203 } |
|
204 \isamarkuptrue% |
|
205 % |
|
206 \begin{isamarkuptext}% |
|
207 We describe the usage of the directory browser and the meaning of |
|
208 the different items in the browser window. |
|
209 |
|
210 \begin{itemize} |
|
211 |
|
212 \item A red arrow before a directory name indicates that the |
|
213 directory is currently ``folded'', i.e.~the nodes in this directory |
|
214 are collapsed to one single node. In the right sub-window, the names |
|
215 of nodes corresponding to folded directories are enclosed in square |
|
216 brackets and displayed in red color. |
|
217 |
|
218 \item A green downward arrow before a directory name indicates that |
|
219 the directory is currently ``unfolded''. It can be folded by |
|
220 clicking on the directory name. Clicking on the name for a second |
|
221 time unfolds the directory again. Alternatively, a directory can |
|
222 also be unfolded by clicking on the corresponding node in the right |
|
223 sub-window. |
|
224 |
|
225 \item Blue arrows stand before ordinary node names. When clicking on |
|
226 such a name (i.e.\ that of a theory), the graph display window |
|
227 focuses to the corresponding node. Double clicking invokes a text |
|
228 viewer window in which the contents of the theory file are |
|
229 displayed. |
|
230 |
|
231 \end{itemize}% |
|
232 \end{isamarkuptext}% |
|
233 \isamarkuptrue% |
|
234 % |
|
235 \isamarkupsubsubsection{The graph display window% |
|
236 } |
|
237 \isamarkuptrue% |
|
238 % |
|
239 \begin{isamarkuptext}% |
|
240 When pointing on an ordinary node, an upward and a downward arrow is |
|
241 shown. Initially, both of these arrows are green. Clicking on the |
|
242 upward or downward arrow collapses all predecessor or successor |
|
243 nodes, respectively. The arrow's color then changes to red, |
|
244 indicating that the predecessor or successor nodes are currently |
|
245 collapsed. The node corresponding to the collapsed nodes has the |
|
246 name ``\verb|[....]|''. To uncollapse the nodes again, simply |
|
247 click on the red arrow or on the node with the name ``\verb|[....]|''. Similar to the directory browser, the contents of |
|
248 theory files can be displayed by double clicking on the |
|
249 corresponding node.% |
|
250 \end{isamarkuptext}% |
|
251 \isamarkuptrue% |
|
252 % |
|
253 \isamarkupsubsubsection{The ``File'' menu% |
|
254 } |
|
255 \isamarkuptrue% |
|
256 % |
|
257 \begin{isamarkuptext}% |
|
258 Due to Java Applet security restrictions this menu is only available |
|
259 in the full application version. The meaning of the menu items is as |
|
260 follows: |
|
261 |
|
262 \begin{description} |
|
263 |
|
264 \item[Open \dots] Open a new graph file. |
|
265 |
|
266 \item[Export to PostScript] Outputs the current graph in Postscript |
|
267 format, appropriately scaled to fit on one single sheet of A4 paper. |
|
268 The resulting file can be printed directly. |
|
269 |
|
270 \item[Export to EPS] Outputs the current graph in Encapsulated |
|
271 Postscript format. The resulting file can be included in other |
|
272 documents. |
|
273 |
|
274 \item[Quit] Quit the graph browser. |
|
275 |
|
276 \end{description}% |
|
277 \end{isamarkuptext}% |
|
278 \isamarkuptrue% |
|
279 % |
|
280 \isamarkupsubsection{Syntax of graph definition files% |
|
281 } |
|
282 \isamarkuptrue% |
|
283 % |
|
284 \begin{isamarkuptext}% |
|
285 A graph definition file has the following syntax: |
|
286 |
|
287 \begin{center}\small |
|
288 \begin{tabular}{rcl} |
|
289 \isa{graph} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}\ vertex{\isaliteral{22}{\isachardoublequote}}}~\verb|;|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}} \\ |
|
290 \isa{vertex} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}vertex{\isaliteral{5F}{\isacharunderscore}}name\ vertex{\isaliteral{5F}{\isacharunderscore}}ID\ dir{\isaliteral{5F}{\isacharunderscore}}name\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}}~\verb|+|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ path\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}}~\verb|<|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~\verb|>|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\ vertex{\isaliteral{5F}{\isacharunderscore}}ID\ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} |
|
291 \end{tabular} |
|
292 \end{center} |
|
293 |
|
294 The meaning of the items in a vertex description is as follows: |
|
295 |
|
296 \begin{description} |
|
297 |
|
298 \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}name}] The name of the vertex. |
|
299 |
|
300 \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}ID}] The vertex identifier. Note that there may |
|
301 be several vertices with equal names, whereas identifiers must be |
|
302 unique. |
|
303 |
|
304 \item[\isa{dir{\isaliteral{5F}{\isacharunderscore}}name}] The name of the ``directory'' the vertex |
|
305 should be placed in. A ``\verb|+|'' sign after \isa{dir{\isaliteral{5F}{\isacharunderscore}}name} indicates that the nodes in the directory are initially |
|
306 visible. Directories are initially invisible by default. |
|
307 |
|
308 \item[\isa{path}] The path of the corresponding theory file. This |
|
309 is specified relatively to the path of the graph definition file. |
|
310 |
|
311 \item[List of successor/predecessor nodes] A ``\verb|<|'' |
|
312 sign before the list means that successor nodes are listed, a |
|
313 ``\verb|>|'' sign means that predecessor nodes are listed. If |
|
314 neither ``\verb|<|'' nor ``\verb|>|'' is found, the |
|
315 browser assumes that successor nodes are listed. |
|
316 |
|
317 \end{description}% |
|
318 \end{isamarkuptext}% |
|
319 \isamarkuptrue% |
|
320 % |
|
321 \isadelimtheory |
|
322 % |
|
323 \endisadelimtheory |
|
324 % |
|
325 \isatagtheory |
|
326 \isacommand{end}\isamarkupfalse% |
|
327 % |
|
328 \endisatagtheory |
|
329 {\isafoldtheory}% |
|
330 % |
|
331 \isadelimtheory |
|
332 % |
|
333 \endisadelimtheory |
|
334 \end{isabellebody}% |
|
335 %%% Local Variables: |
|
336 %%% mode: latex |
|
337 %%% TeX-master: "root" |
|
338 %%% End: |
|