author | wenzelm |
Wed, 15 Aug 2012 12:36:38 +0200 | |
changeset 48814 | d488a5f25bf6 |
parent 48791 | 9e8f30bfbdca |
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 |
|
11 |
with some components to provide a fully-featured Prover IDE: |
|
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 |
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 |
|
48791 | 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. |
|
48573 | 34 |
|
35 |
The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass |
|
36 |
additional low-level options to the JVM or jEdit, respectively. The |
|
48603 | 37 |
defaults are provided by the Isabelle settings environment |
38 |
(\secref{sec:settings}). |
|
48573 | 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 |
|
48603 | 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. *} |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
47 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
48 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
49 |
section {* Proof General / Emacs *} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
50 |
|
48572 | 51 |
text {* The @{tool_def emacs} tool invokes a version of Emacs and |
48603 | 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. |
|
28916
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 |
The actual interface script is part of the Proof General |
48572 | 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: |
|
28916
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 |
\begin{description} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
66 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
67 |
\item[@{setting_def PROOFGENERAL_HOME}] points to the main |
48572 | 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. |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
72 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
73 |
\item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
74 |
the command line of any invocation of the Proof General @{verbatim |
48572 | 75 |
interface} script. This allows to provide persistent default |
76 |
options for the invocation of \texttt{isabelle emacs}. |
|
28916
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 |
\end{description} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
79 |
*} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
80 |
|
47824 | 81 |
|
48573 | 82 |
section {* Plain TTY interaction \label{sec:tool-tty} *} |
47824 | 83 |
|
48573 | 84 |
text {* |
85 |
The @{tool_def tty} tool runs the Isabelle process interactively |
|
86 |
within a plain terminal session: |
|
47824 | 87 |
\begin{ttbox} |
48573 | 88 |
Usage: isabelle tty [OPTIONS] |
47824 | 89 |
|
90 |
Options are: |
|
91 |
-l NAME logic image name (default ISABELLE_LOGIC) |
|
92 |
-m MODE add print mode for output |
|
48573 | 93 |
-p NAME line editor program name (default ISABELLE_LINE_EDITOR) |
47824 | 94 |
|
48573 | 95 |
Run Isabelle process with plain tty interaction and line editor. |
47824 | 96 |
\end{ttbox} |
97 |
||
48573 | 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. |
|
47824 | 103 |
|
48603 | 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. *} |
|
47824 | 109 |
|
48576 | 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 |
|
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
|
119 |
a stand-alone application and as an applet. *} |
48576 | 120 |
|
121 |
||
122 |
subsection {* Invoking the graph browser *} |
|
123 |
||
48602 | 124 |
text {* The stand-alone version of the graph browser is wrapped up as |
125 |
@{tool_def browser}: |
|
48576 | 126 |
\begin{ttbox} |
48602 | 127 |
Usage: isabelle browser [OPTIONS] [GRAPHFILE] |
48576 | 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 |
||
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
281 |
end |