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