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