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