author | wenzelm |
Mon, 30 Jul 2012 14:11:29 +0200 | |
changeset 48602 | 342ca8f3197b |
parent 48577 | 1edc81c78079 |
child 48722 | a5e3ba7cbb2a |
permissions | -rw-r--r-- |
28224 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Misc}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Misc\isanewline |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
41512
diff
changeset
|
12 |
\isakeyword{imports}\ Base\isanewline |
28224 | 13 |
\isakeyword{begin}% |
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Miscellaneous tools \label{ch:tools}% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\begin{isamarkuptext}% |
|
26 |
Subsequently we describe various Isabelle related utilities, given |
|
27 |
in alphabetical order.% |
|
28 |
\end{isamarkuptext}% |
|
29 |
\isamarkuptrue% |
|
30 |
% |
|
31 |
\isamarkupsection{Displaying documents% |
|
32 |
} |
|
33 |
\isamarkuptrue% |
|
34 |
% |
|
35 |
\begin{isamarkuptext}% |
|
48602 | 36 |
The \indexdef{}{tool}{display}\hypertarget{tool.display}{\hyperlink{tool.display}{\mbox{\isa{\isatool{display}}}}} tool displays documents in DVI or PDF |
28224 | 37 |
format: |
38 |
\begin{ttbox} |
|
48602 | 39 |
Usage: isabelle display [OPTIONS] FILE |
28224 | 40 |
|
41 |
Options are: |
|
42 |
-c cleanup -- remove FILE after use |
|
43 |
||
44 |
Display document FILE (in DVI format). |
|
45 |
\end{ttbox} |
|
46 |
||
47 |
\medskip The \verb|-c| option causes the input file to be |
|
48 |
removed after use. The program for viewing \verb|dvi| files is |
|
40406 | 49 |
determined by the \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.% |
28224 | 50 |
\end{isamarkuptext}% |
51 |
\isamarkuptrue% |
|
52 |
% |
|
53 |
\isamarkupsection{Viewing documentation \label{sec:tool-doc}% |
|
54 |
} |
|
55 |
\isamarkuptrue% |
|
56 |
% |
|
57 |
\begin{isamarkuptext}% |
|
48602 | 58 |
The \indexdef{}{tool}{doc}\hypertarget{tool.doc}{\hyperlink{tool.doc}{\mbox{\isa{\isatool{doc}}}}} tool displays online documentation: |
28224 | 59 |
\begin{ttbox} |
48602 | 60 |
Usage: isabelle doc [DOC] |
28224 | 61 |
|
62 |
View Isabelle documentation DOC, or show list of available documents. |
|
63 |
\end{ttbox} |
|
64 |
If called without arguments, it lists all available documents. Each |
|
65 |
line starts with an identifier, followed by a short description. Any |
|
66 |
of these identifiers may be specified as the first argument in order |
|
67 |
to have the corresponding document displayed. |
|
68 |
||
40406 | 69 |
\medskip The \hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCS}}}} setting specifies the list of |
28224 | 70 |
directories (separated by colons) to be scanned for documentations. |
71 |
The program for viewing \verb|dvi| files is determined by the |
|
40406 | 72 |
\hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.% |
28224 | 73 |
\end{isamarkuptext}% |
74 |
\isamarkuptrue% |
|
75 |
% |
|
47828 | 76 |
\isamarkupsection{Shell commands within the settings environment \label{sec:tool-env}% |
77 |
} |
|
78 |
\isamarkuptrue% |
|
79 |
% |
|
80 |
\begin{isamarkuptext}% |
|
48602 | 81 |
The \indexdef{}{tool}{env}\hypertarget{tool.env}{\hyperlink{tool.env}{\mbox{\isa{\isatool{env}}}}} tool is a direct wrapper for the standard |
82 |
\verb|/usr/bin/env| command on POSIX systems, running within |
|
83 |
the Isabelle settings environment (\secref{sec:settings}). |
|
47828 | 84 |
|
85 |
The command-line arguments are that of the underlying version of |
|
86 |
\verb|env|. For example, the following invokes an instance of |
|
87 |
the GNU Bash shell within the Isabelle environment: |
|
88 |
\begin{alltt} |
|
89 |
isabelle env bash |
|
90 |
\end{alltt}% |
|
91 |
\end{isamarkuptext}% |
|
92 |
\isamarkuptrue% |
|
93 |
% |
|
28224 | 94 |
\isamarkupsection{Getting logic images% |
95 |
} |
|
96 |
\isamarkuptrue% |
|
97 |
% |
|
98 |
\begin{isamarkuptext}% |
|
48602 | 99 |
The \indexdef{}{tool}{findlogics}\hypertarget{tool.findlogics}{\hyperlink{tool.findlogics}{\mbox{\isa{\isatool{findlogics}}}}} tool traverses all directories |
40406 | 100 |
specified in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}}, looking for Isabelle logic |
28224 | 101 |
images. Its usage is: |
102 |
\begin{ttbox} |
|
48577 | 103 |
Usage: isabelle findlogics |
28224 | 104 |
|
105 |
Collect heap file names from ISABELLE_PATH. |
|
106 |
\end{ttbox} |
|
107 |
||
108 |
The base names of all files found on the path are printed --- sorted |
|
40406 | 109 |
and with duplicates removed. Also note that lookup in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}} includes the current values of \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} |
110 |
and \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}. Thus switching to another ML compiler |
|
28224 | 111 |
may change the set of logic images available.% |
112 |
\end{isamarkuptext}% |
|
113 |
\isamarkuptrue% |
|
114 |
% |
|
115 |
\isamarkupsection{Inspecting the settings environment \label{sec:tool-getenv}% |
|
116 |
} |
|
117 |
\isamarkuptrue% |
|
118 |
% |
|
119 |
\begin{isamarkuptext}% |
|
120 |
The Isabelle settings environment --- as provided by the |
|
121 |
site-default and user-specific settings files --- can be inspected |
|
48602 | 122 |
with the \indexdef{}{tool}{getenv}\hypertarget{tool.getenv}{\hyperlink{tool.getenv}{\mbox{\isa{\isatool{getenv}}}}} tool: |
28224 | 123 |
\begin{ttbox} |
48602 | 124 |
Usage: isabelle getenv [OPTIONS] [VARNAMES ...] |
28224 | 125 |
|
126 |
Options are: |
|
127 |
-a display complete environment |
|
128 |
-b print values only (doesn't work for -a) |
|
31497 | 129 |
-d FILE dump complete environment to FILE |
130 |
(null terminated entries) |
|
28224 | 131 |
|
132 |
Get value of VARNAMES from the Isabelle settings. |
|
133 |
\end{ttbox} |
|
134 |
||
135 |
With the \verb|-a| option, one may inspect the full process |
|
136 |
environment that Isabelle related programs are run in. This usually |
|
137 |
contains much more variables than are actually Isabelle settings. |
|
138 |
Normally, output is a list of lines of the form \isa{name}\verb|=|\isa{value}. The \verb|-b| option |
|
31497 | 139 |
causes only the values to be printed. |
140 |
||
141 |
Option \verb|-d| produces a dump of the complete environment |
|
142 |
to the specified file. Entries are terminated by the ASCII null |
|
143 |
character, i.e.\ the C string terminator.% |
|
28224 | 144 |
\end{isamarkuptext}% |
145 |
\isamarkuptrue% |
|
146 |
% |
|
147 |
\isamarkupsubsubsection{Examples% |
|
148 |
} |
|
149 |
\isamarkuptrue% |
|
150 |
% |
|
151 |
\begin{isamarkuptext}% |
|
152 |
Get the ML system name and the location where the compiler binaries |
|
153 |
are supposed to reside as follows: |
|
154 |
\begin{ttbox} |
|
28505 | 155 |
isabelle getenv ML_SYSTEM ML_HOME |
28224 | 156 |
{\out ML_SYSTEM=polyml} |
157 |
{\out ML_HOME=/usr/share/polyml/x86-linux} |
|
158 |
\end{ttbox} |
|
159 |
||
160 |
The next one peeks at the output directory for Isabelle logic |
|
161 |
images: |
|
162 |
\begin{ttbox} |
|
28505 | 163 |
isabelle getenv -b ISABELLE_OUTPUT |
28224 | 164 |
{\out /home/me/isabelle/heaps/polyml_x86-linux} |
165 |
\end{ttbox} |
|
166 |
Here we have used the \verb|-b| option to suppress the |
|
167 |
\verb|ISABELLE_OUTPUT=| prefix. The value above is what |
|
168 |
became of the following assignment in the default settings file: |
|
169 |
\begin{ttbox} |
|
170 |
ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps" |
|
171 |
\end{ttbox} |
|
172 |
||
40406 | 173 |
Note how the \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}} value got appended |
28224 | 174 |
automatically to each path component. This is a special feature of |
40406 | 175 |
\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}}.% |
28224 | 176 |
\end{isamarkuptext}% |
177 |
\isamarkuptrue% |
|
178 |
% |
|
179 |
\isamarkupsection{Installing standalone Isabelle executables \label{sec:tool-install}% |
|
180 |
} |
|
181 |
\isamarkuptrue% |
|
182 |
% |
|
183 |
\begin{isamarkuptext}% |
|
48602 | 184 |
By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} etc.) are just run from their location within the |
185 |
distribution directory, probably indirectly by the shell through its |
|
186 |
\hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}. Other schemes of installation are supported by the |
|
187 |
\indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatool{install}}}}} tool: |
|
28224 | 188 |
\begin{ttbox} |
48602 | 189 |
Usage: isabelle install [OPTIONS] |
28224 | 190 |
|
191 |
Options are: |
|
192 |
-d DISTDIR use DISTDIR as Isabelle distribution |
|
193 |
(default ISABELLE_HOME) |
|
194 |
-p DIR install standalone binaries in DIR |
|
195 |
||
196 |
Install Isabelle executables with absolute references to the current |
|
197 |
distribution directory. |
|
198 |
\end{ttbox} |
|
199 |
||
200 |
The \verb|-d| option overrides the current Isabelle |
|
40406 | 201 |
distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}. |
28224 | 202 |
|
203 |
The \verb|-p| option installs executable wrapper scripts for |
|
40406 | 204 |
\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}, |
28238 | 205 |
\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the |
206 |
Isabelle distribution directory. A typical \verb|DIR| |
|
207 |
specification would be some directory expected to be in the shell's |
|
208 |
\hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}, such as \verb|/usr/local/bin|. It is |
|
209 |
important to note that a plain manual copy of the original Isabelle |
|
210 |
executables does not work, since it disrupts the integrity of the |
|
211 |
Isabelle distribution.% |
|
28224 | 212 |
\end{isamarkuptext}% |
213 |
\isamarkuptrue% |
|
214 |
% |
|
215 |
\isamarkupsection{Creating instances of the Isabelle logo% |
|
216 |
} |
|
217 |
\isamarkuptrue% |
|
218 |
% |
|
219 |
\begin{isamarkuptext}% |
|
48602 | 220 |
The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatool{logo}}}}} tool creates any instance of the generic |
28224 | 221 |
Isabelle logo as an Encapsuled Postscript file (EPS): |
222 |
\begin{ttbox} |
|
48602 | 223 |
Usage: isabelle logo [OPTIONS] NAME |
28224 | 224 |
|
225 |
Create instance NAME of the Isabelle logo (as EPS). |
|
226 |
||
227 |
Options are: |
|
228 |
-o OUTFILE set output file (default determined from NAME) |
|
229 |
-q quiet mode |
|
230 |
\end{ttbox} |
|
231 |
You are encouraged to use this to create a derived logo for your |
|
48602 | 232 |
Isabelle project. For example, \hyperlink{tool.logo}{\mbox{\isa{\isatool{logo}}}}~\verb|Bali| |
233 |
creates \verb|isabelle_bali.eps|.% |
|
28224 | 234 |
\end{isamarkuptext}% |
235 |
\isamarkuptrue% |
|
236 |
% |
|
237 |
\isamarkupsection{Isabelle's version of make \label{sec:tool-make}% |
|
238 |
} |
|
239 |
\isamarkuptrue% |
|
240 |
% |
|
241 |
\begin{isamarkuptext}% |
|
48602 | 242 |
The \indexdef{}{tool}{make}\hypertarget{tool.make}{\hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}}} tool is a very simple wrapper for |
28224 | 243 |
ordinary Unix \hyperlink{executable.make}{\mbox{\isa{\isatt{make}}}}: |
244 |
\begin{ttbox} |
|
48602 | 245 |
Usage: isabelle make [ARGS ...] |
28224 | 246 |
|
247 |
Compile the logic in current directory using IsaMakefile. |
|
248 |
ARGS are directly passed to the system make program. |
|
249 |
\end{ttbox} |
|
250 |
||
251 |
Note that the Isabelle settings environment is also active. Thus one |
|
252 |
may refer to its values within the \verb|IsaMakefile|, e.g.\ |
|
253 |
\verb|$(ISABELLE_OUTPUT)|. Furthermore, programs started from |
|
48602 | 254 |
the make file also inherit this environment. Typically, \verb|IsaMakefile|s defer the real work to \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}. |
28224 | 255 |
|
256 |
\medskip The basic \verb|IsaMakefile| convention is that the |
|
257 |
default target builds the actual logic, including its parents if |
|
258 |
appropriate. The \verb|images| target is intended to build all |
|
259 |
local logic images, while the \verb|test| target shall build |
|
260 |
all related examples. The \verb|all| target shall do |
|
261 |
\verb|images| and \verb|test|.% |
|
262 |
\end{isamarkuptext}% |
|
263 |
\isamarkuptrue% |
|
264 |
% |
|
265 |
\isamarkupsubsubsection{Examples% |
|
266 |
} |
|
267 |
\isamarkuptrue% |
|
268 |
% |
|
269 |
\begin{isamarkuptext}% |
|
270 |
Refer to the \verb|IsaMakefile|s of the Isabelle distribution's |
|
271 |
object-logics as a model for your own developments. For example, |
|
40802 | 272 |
see \verb|~~/src/FOL/IsaMakefile|.% |
28224 | 273 |
\end{isamarkuptext}% |
274 |
\isamarkuptrue% |
|
275 |
% |
|
276 |
\isamarkupsection{Make all logics% |
|
277 |
} |
|
278 |
\isamarkuptrue% |
|
279 |
% |
|
280 |
\begin{isamarkuptext}% |
|
48602 | 281 |
The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatool{makeall}}}}} tool applies Isabelle make to any |
32325 | 282 |
Isabelle component (cf.\ \secref{sec:components}) that contains an |
283 |
\verb|IsaMakefile|: |
|
28224 | 284 |
\begin{ttbox} |
48602 | 285 |
Usage: isabelle makeall [ARGS ...] |
28224 | 286 |
|
32325 | 287 |
Apply isabelle make to all components with IsaMakefile (passing ARGS). |
28224 | 288 |
\end{ttbox} |
289 |
||
290 |
The arguments \verb|ARGS| are just passed verbatim to each |
|
48602 | 291 |
\hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}} invocation.% |
28224 | 292 |
\end{isamarkuptext}% |
293 |
\isamarkuptrue% |
|
294 |
% |
|
295 |
\isamarkupsection{Printing documents% |
|
296 |
} |
|
297 |
\isamarkuptrue% |
|
298 |
% |
|
299 |
\begin{isamarkuptext}% |
|
48602 | 300 |
The \indexdef{}{tool}{print}\hypertarget{tool.print}{\hyperlink{tool.print}{\mbox{\isa{\isatool{print}}}}} tool prints documents: |
28224 | 301 |
\begin{ttbox} |
48602 | 302 |
Usage: isabelle print [OPTIONS] FILE |
28224 | 303 |
|
304 |
Options are: |
|
305 |
-c cleanup -- remove FILE after use |
|
306 |
||
307 |
Print document FILE. |
|
308 |
\end{ttbox} |
|
309 |
||
310 |
The \verb|-c| option causes the input file to be removed |
|
40406 | 311 |
after use. The printer spool command is determined by the \hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isaliteral{5F}{\isacharunderscore}}COMMAND}}}} setting.% |
28224 | 312 |
\end{isamarkuptext}% |
313 |
\isamarkuptrue% |
|
314 |
% |
|
315 |
\isamarkupsection{Remove awkward symbol names from theory sources% |
|
316 |
} |
|
317 |
\isamarkuptrue% |
|
318 |
% |
|
319 |
\begin{isamarkuptext}% |
|
48602 | 320 |
The \indexdef{}{tool}{unsymbolize}\hypertarget{tool.unsymbolize}{\hyperlink{tool.unsymbolize}{\mbox{\isa{\isatool{unsymbolize}}}}} tool tunes Isabelle theory sources to |
28224 | 321 |
improve readability for plain ASCII output (e.g.\ in email |
48602 | 322 |
communication). Most notably, \hyperlink{tool.unsymbolize}{\mbox{\isa{\isatool{unsymbolize}}}} replaces awkward |
28224 | 323 |
arrow symbols such as \verb|\|\verb|<Longrightarrow>| |
324 |
by \verb|==>|. |
|
325 |
\begin{ttbox} |
|
48602 | 326 |
Usage: isabelle unsymbolize [FILES|DIRS...] |
28224 | 327 |
|
328 |
Recursively find .thy/.ML files, removing unreadable symbol names. |
|
329 |
Note: this is an ad-hoc script; there is no systematic way to replace |
|
330 |
symbols independently of the inner syntax of a theory! |
|
331 |
||
332 |
Renames old versions of FILES by appending "~~". |
|
333 |
\end{ttbox}% |
|
334 |
\end{isamarkuptext}% |
|
335 |
\isamarkuptrue% |
|
336 |
% |
|
337 |
\isamarkupsection{Output the version identifier of the Isabelle distribution% |
|
338 |
} |
|
339 |
\isamarkuptrue% |
|
340 |
% |
|
341 |
\begin{isamarkuptext}% |
|
48602 | 342 |
The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatool{version}}}}} tool displays Isabelle version information: |
41511 | 343 |
\begin{ttbox} |
344 |
Usage: isabelle version [OPTIONS] |
|
345 |
||
346 |
Options are: |
|
347 |
-i short identification (derived from Mercurial id) |
|
348 |
||
349 |
Display Isabelle version information. |
|
350 |
\end{ttbox} |
|
351 |
||
352 |
\medskip The default is to output the full version string of the |
|
47827 | 353 |
Isabelle distribution, e.g.\ ``\verb|Isabelle2012: May 2012|. |
41511 | 354 |
|
355 |
The \verb|-i| option produces a short identification derived |
|
356 |
from the Mercurial id of the \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} directory.% |
|
28224 | 357 |
\end{isamarkuptext}% |
358 |
\isamarkuptrue% |
|
359 |
% |
|
360 |
\isamarkupsection{Convert XML to YXML% |
|
361 |
} |
|
362 |
\isamarkuptrue% |
|
363 |
% |
|
364 |
\begin{isamarkuptext}% |
|
48602 | 365 |
The \indexdef{}{tool}{yxml}\hypertarget{tool.yxml}{\hyperlink{tool.yxml}{\mbox{\isa{\isatool{yxml}}}}} tool converts a standard XML document (stdin) |
28224 | 366 |
to the much simpler and more efficient YXML format of Isabelle |
367 |
(stdout). The YXML format is defined as follows. |
|
368 |
||
369 |
\begin{enumerate} |
|
370 |
||
371 |
\item The encoding is always UTF-8. |
|
372 |
||
373 |
\item Body text is represented verbatim (no escaping, no special |
|
374 |
treatment of white space, no named entities, no CDATA chunks, no |
|
375 |
comments). |
|
376 |
||
377 |
\item Markup elements are represented via ASCII control characters |
|
40406 | 378 |
\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{5}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{6}}{\isaliteral{22}{\isachardoublequote}}} as follows: |
28224 | 379 |
|
380 |
\begin{tabular}{ll} |
|
381 |
XML & YXML \\\hline |
|
40406 | 382 |
\verb|<|\isa{{\isaliteral{22}{\isachardoublequote}}name\ attribute{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}\verb|>| & |
383 |
\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Yname\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Yattribute{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value{\isaliteral{5C3C646F74733E}{\isasymdots}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} \\ |
|
384 |
\verb|</|\isa{name}\verb|>| & \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} \\ |
|
28224 | 385 |
\end{tabular} |
386 |
||
387 |
There is no special case for empty body text, i.e.\ \verb|<foo/>| is treated like \verb|<foo></foo>|. Also note that |
|
40406 | 388 |
\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}} may never occur in |
28224 | 389 |
well-formed XML documents. |
390 |
||
391 |
\end{enumerate} |
|
392 |
||
393 |
Parsing YXML is pretty straight-forward: split the text into chunks |
|
40406 | 394 |
separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}}, then split each chunk into |
395 |
sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start |
|
28224 | 396 |
with an empty sub-chunk, and a second empty sub-chunk indicates |
397 |
close of an element. Any other non-empty chunk consists of plain |
|
44799 | 398 |
text. For example, see \verb|~~/src/Pure/PIDE/yxml.ML| or |
399 |
\verb|~~/src/Pure/PIDE/yxml.scala|. |
|
28224 | 400 |
|
401 |
YXML documents may be detected quickly by checking that the first |
|
40406 | 402 |
two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.% |
28224 | 403 |
\end{isamarkuptext}% |
404 |
\isamarkuptrue% |
|
405 |
% |
|
406 |
\isadelimtheory |
|
407 |
% |
|
408 |
\endisadelimtheory |
|
409 |
% |
|
410 |
\isatagtheory |
|
411 |
\isacommand{end}\isamarkupfalse% |
|
412 |
% |
|
413 |
\endisatagtheory |
|
414 |
{\isafoldtheory}% |
|
415 |
% |
|
416 |
\isadelimtheory |
|
417 |
% |
|
418 |
\endisadelimtheory |
|
419 |
\end{isabellebody}% |
|
420 |
%%% Local Variables: |
|
421 |
%%% mode: latex |
|
422 |
%%% TeX-master: "root" |
|
423 |
%%% End: |