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 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
2 |
\begin{isabellebody}% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
3 |
\def\isabellecontext{Interfaces}% |
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 |
\isadelimtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
6 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
7 |
\endisadelimtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
8 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
9 |
\isatagtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
10 |
\isacommand{theory}\isamarkupfalse% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
11 |
\ Interfaces\isanewline |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
12 |
\isakeyword{imports}\ Base\isanewline |
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
13 |
\isakeyword{begin}% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
14 |
\endisatagtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
15 |
{\isafoldtheory}% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
16 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
17 |
\isadelimtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
18 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
19 |
\endisadelimtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
20 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
21 |
\isamarkupchapter{User interfaces% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
22 |
} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
23 |
\isamarkuptrue% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
24 |
% |
48573 | 25 |
\isamarkupsection{Isabelle/jEdit Prover IDE \label{sec:tool-jedit}% |
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
26 |
} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
27 |
\isamarkuptrue% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
28 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
29 |
\begin{isamarkuptext}% |
48603 | 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 ...] |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
35 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
36 |
Options are: |
48573 | 37 |
-J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS) |
38 |
-b build only |
|
48791 | 39 |
-d DIR include session directory |
48573 | 40 |
-f fresh build |
41 |
-j OPTION add jEdit runtime option (default JEDIT_OPTIONS) |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
42 |
-l NAME logic image name (default ISABELLE_LOGIC) |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
43 |
-m MODE add print mode for output |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
44 |
|
48573 | 45 |
Start jEdit with Isabelle plugin setup and opens theory FILES |
46 |
(default Scratch.thy). |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
47 |
\end{ttbox} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
48 |
|
48791 | 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. |
|
48573 | 55 |
|
56 |
The \verb|-J| and \verb|-j| options allow to pass |
|
57 |
additional low-level options to the JVM or jEdit, respectively. The |
|
48603 | 58 |
defaults are provided by the Isabelle settings environment |
59 |
(\secref{sec:settings}). |
|
48573 | 60 |
|
61 |
The \verb|-b| and \verb|-f| options control the |
|
62 |
self-build mechanism of Isabelle/jEdit. This is only relevant for |
|
48603 | 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.% |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
67 |
\end{isamarkuptext}% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
68 |
\isamarkuptrue% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
69 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
70 |
\isamarkupsection{Proof General / Emacs% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
71 |
} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
72 |
\isamarkuptrue% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
73 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
74 |
\begin{isamarkuptext}% |
48602 | 75 |
The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatool{emacs}}}}} tool invokes a version of Emacs and |
48603 | 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. |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
81 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
82 |
The actual interface script is part of the Proof General |
48572 | 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: |
|
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 |
\begin{description} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
90 |
|
40406 | 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 |
48572 | 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. |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
96 |
|
40406 | 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 |
48572 | 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}. |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
100 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
101 |
\end{description}% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
102 |
\end{isamarkuptext}% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
103 |
\isamarkuptrue% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
104 |
% |
48573 | 105 |
\isamarkupsection{Plain TTY interaction \label{sec:tool-tty}% |
47824 | 106 |
} |
107 |
\isamarkuptrue% |
|
108 |
% |
|
109 |
\begin{isamarkuptext}% |
|
48602 | 110 |
The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatool{tty}}}}} tool runs the Isabelle process interactively |
48573 | 111 |
within a plain terminal session: |
47824 | 112 |
\begin{ttbox} |
48573 | 113 |
Usage: isabelle tty [OPTIONS] |
47824 | 114 |
|
115 |
Options are: |
|
116 |
-l NAME logic image name (default ISABELLE_LOGIC) |
|
117 |
-m MODE add print mode for output |
|
48573 | 118 |
-p NAME line editor program name (default ISABELLE_LINE_EDITOR) |
47824 | 119 |
|
48573 | 120 |
Run Isabelle process with plain tty interaction and line editor. |
47824 | 121 |
\end{ttbox} |
122 |
||
48573 | 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. |
|
47824 | 128 |
|
48603 | 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.% |
|
47824 | 133 |
\end{isamarkuptext}% |
134 |
\isamarkuptrue% |
|
135 |
% |
|
48576 | 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 |
|
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
|
146 |
a stand-alone application and as an applet.% |
48576 | 147 |
\end{isamarkuptext}% |
148 |
\isamarkuptrue% |
|
149 |
% |
|
150 |
\isamarkupsubsection{Invoking the graph browser% |
|
151 |
} |
|
152 |
\isamarkuptrue% |
|
153 |
% |
|
154 |
\begin{isamarkuptext}% |
|
48602 | 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}}}}}: |
|
48576 | 157 |
\begin{ttbox} |
48602 | 158 |
Usage: isabelle browser [OPTIONS] [GRAPHFILE] |
48576 | 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 |
% |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
321 |
\isadelimtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
322 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
323 |
\endisadelimtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
324 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
325 |
\isatagtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
326 |
\isacommand{end}\isamarkupfalse% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
327 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
328 |
\endisatagtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
329 |
{\isafoldtheory}% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
330 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
331 |
\isadelimtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
332 |
% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
333 |
\endisadelimtheory |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
334 |
\end{isabellebody}% |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
335 |
%%% Local Variables: |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
336 |
%%% mode: latex |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
337 |
%%% TeX-master: "root" |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
338 |
%%% End: |