author | wenzelm |
Thu, 31 Dec 2015 19:53:19 +0100 | |
changeset 62013 | 92a2372a226b |
parent 61656 | cfabbc083977 |
child 62451 | 040b94ffbdde |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
61575 | 2 |
|
28224 | 3 |
theory Misc |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
41512
diff
changeset
|
4 |
imports Base |
28224 | 5 |
begin |
6 |
||
58618 | 7 |
chapter \<open>Miscellaneous tools \label{ch:tools}\<close> |
28224 | 8 |
|
58618 | 9 |
text \<open> |
61575 | 10 |
Subsequently we describe various Isabelle related utilities, given in |
11 |
alphabetical order. |
|
58618 | 12 |
\<close> |
28224 | 13 |
|
14 |
||
58618 | 15 |
section \<open>Resolving Isabelle components \label{sec:tool-components}\<close> |
48844 | 16 |
|
58618 | 17 |
text \<open> |
48844 | 18 |
The @{tool_def components} tool resolves Isabelle components: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
19 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
20 |
\<open>Usage: isabelle components [OPTIONS] [COMPONENTS ...] |
48844 | 21 |
|
22 |
Options are: |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50132
diff
changeset
|
23 |
-I init user settings |
48844 | 24 |
-R URL component repository |
25 |
(default $ISABELLE_COMPONENT_REPOSITORY) |
|
53435 | 26 |
-a resolve all missing components |
48844 | 27 |
-l list status |
28 |
||
29 |
Resolve Isabelle components via download and installation. |
|
30 |
COMPONENTS are identified via base name. |
|
31 |
||
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
32 |
ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"\<close>} |
48844 | 33 |
|
61575 | 34 |
Components are initialized as described in \secref{sec:components} in a |
35 |
permissive manner, which can mark components as ``missing''. This state is |
|
36 |
amended by letting @{tool "components"} download and unpack components that |
|
37 |
are published on the default component repository @{url |
|
38 |
"http://isabelle.in.tum.de/components/"} in particular. |
|
48844 | 39 |
|
61575 | 40 |
Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that |
41 |
\<^verbatim>\<open>file:///\<close> URLs can be used for local directories. |
|
48844 | 42 |
|
61575 | 43 |
Option \<^verbatim>\<open>-a\<close> selects all missing components to be resolved. Explicit |
44 |
components may be named as command line-arguments as well. Note that |
|
45 |
components are uniquely identified by their base name, while the |
|
46 |
installation takes place in the location that was specified in the attempt |
|
47 |
to initialize the component before. |
|
48844 | 48 |
|
61575 | 49 |
Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components |
50 |
with their location (full name) within the file-system. |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50132
diff
changeset
|
51 |
|
61575 | 52 |
Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard |
53 |
components specified in the Isabelle repository clone --- this does not make |
|
54 |
any sense for regular Isabelle releases. If the file already exists, it |
|
55 |
needs to be edited manually according to the printed explanation. |
|
58618 | 56 |
\<close> |
48844 | 57 |
|
58 |
||
58618 | 59 |
section \<open>Raw ML console\<close> |
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
60 |
|
58618 | 61 |
text \<open> |
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
62 |
The @{tool_def console} tool runs the Isabelle process with raw ML console: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
63 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
64 |
\<open>Usage: isabelle console [OPTIONS] |
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
65 |
|
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
66 |
Options are: |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
67 |
-d DIR include session directory |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
68 |
-l NAME logic session name (default ISABELLE_LOGIC) |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
69 |
-m MODE add print mode for output |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
70 |
-n no build of session image on startup |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
71 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
72 |
-s system build mode for session image |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
73 |
|
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
74 |
Run Isabelle process with raw ML console and line editor |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
75 |
(default ISABELLE_LINE_EDITOR).\<close>} |
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
76 |
|
61575 | 77 |
The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default, its heap |
78 |
image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. |
|
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
79 |
|
61575 | 80 |
Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed directly to @{tool build} |
81 |
(\secref{sec:tool-build}). |
|
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
82 |
|
61575 | 83 |
Options \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> are passed directly to the underlying Isabelle process |
84 |
(\secref{sec:isabelle-process}). |
|
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
85 |
|
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
86 |
The Isabelle process is run through the line editor that is specified via |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
87 |
the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\ |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
88 |
@{executable_def rlwrap} for GNU readline); the fall-back is to use plain |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
89 |
standard input/output. |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
90 |
|
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
91 |
Interaction works via the raw ML toplevel loop: this is neither |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
92 |
Isabelle/Isar nor Isabelle/ML within the usual formal context. Some useful |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
93 |
ML commands at this stage are @{ML cd}, @{ML pwd}, @{ML use}, @{ML use_thy}, |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
94 |
@{ML use_thys}. |
58618 | 95 |
\<close> |
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
96 |
|
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57414
diff
changeset
|
97 |
|
58618 | 98 |
section \<open>Displaying documents \label{sec:tool-display}\<close> |
28224 | 99 |
|
61575 | 100 |
text \<open> |
101 |
The @{tool_def display} tool displays documents in DVI or PDF format: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
102 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
103 |
\<open>Usage: isabelle display DOCUMENT |
28224 | 104 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
105 |
Display DOCUMENT (in DVI or PDF format).\<close>} |
28224 | 106 |
|
61406 | 107 |
\<^medskip> |
61575 | 108 |
The settings @{setting DVI_VIEWER} and @{setting PDF_VIEWER} determine the |
109 |
programs for viewing the corresponding file formats. Normally this opens the |
|
110 |
document via the desktop environment, potentially in an asynchronous manner |
|
111 |
with re-use of previews views. |
|
58618 | 112 |
\<close> |
28224 | 113 |
|
114 |
||
58618 | 115 |
section \<open>Viewing documentation \label{sec:tool-doc}\<close> |
28224 | 116 |
|
58618 | 117 |
text \<open> |
52444
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents:
52052
diff
changeset
|
118 |
The @{tool_def doc} tool displays Isabelle documentation: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
119 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
120 |
\<open>Usage: isabelle doc [DOC ...] |
28224 | 121 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
122 |
View Isabelle documentation.\<close>} |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
123 |
|
61575 | 124 |
If called without arguments, it lists all available documents. Each line |
125 |
starts with an identifier, followed by a short description. Any of these |
|
126 |
identifiers may be specified as arguments, in order to display the |
|
127 |
corresponding document (see also \secref{sec:tool-display}). |
|
28224 | 128 |
|
61406 | 129 |
\<^medskip> |
61575 | 130 |
The @{setting ISABELLE_DOCS} setting specifies the list of directories |
131 |
(separated by colons) to be scanned for documentations. |
|
58618 | 132 |
\<close> |
28224 | 133 |
|
134 |
||
58618 | 135 |
section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close> |
47828 | 136 |
|
61575 | 137 |
text \<open> |
138 |
The @{tool_def env} tool is a direct wrapper for the standard |
|
139 |
\<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within the Isabelle |
|
140 |
settings environment (\secref{sec:settings}). |
|
47828 | 141 |
|
61575 | 142 |
The command-line arguments are that of the underlying version of \<^verbatim>\<open>env\<close>. For |
143 |
example, the following invokes an instance of the GNU Bash shell within the |
|
144 |
Isabelle environment: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
145 |
@{verbatim [display] \<open>isabelle env bash\<close>} |
58618 | 146 |
\<close> |
47828 | 147 |
|
148 |
||
58618 | 149 |
section \<open>Inspecting the settings environment \label{sec:tool-getenv}\<close> |
28224 | 150 |
|
58618 | 151 |
text \<open>The Isabelle settings environment --- as provided by the |
28224 | 152 |
site-default and user-specific settings files --- can be inspected |
48602 | 153 |
with the @{tool_def getenv} tool: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
154 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
155 |
\<open>Usage: isabelle getenv [OPTIONS] [VARNAMES ...] |
28224 | 156 |
|
157 |
Options are: |
|
158 |
-a display complete environment |
|
159 |
-b print values only (doesn't work for -a) |
|
31497 | 160 |
-d FILE dump complete environment to FILE |
161 |
(null terminated entries) |
|
28224 | 162 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
163 |
Get value of VARNAMES from the Isabelle settings.\<close>} |
28224 | 164 |
|
61575 | 165 |
With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process environment that |
166 |
Isabelle related programs are run in. This usually contains much more |
|
167 |
variables than are actually Isabelle settings. Normally, output is a list of |
|
168 |
lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option causes only the values |
|
169 |
to be printed. |
|
31497 | 170 |
|
61575 | 171 |
Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment to the specified |
172 |
file. Entries are terminated by the ASCII null character, i.e.\ the C string |
|
173 |
terminator. |
|
58618 | 174 |
\<close> |
28224 | 175 |
|
176 |
||
58618 | 177 |
subsubsection \<open>Examples\<close> |
28224 | 178 |
|
61575 | 179 |
text \<open> |
180 |
Get the location of @{setting ISABELLE_HOME_USER} where user-specific |
|
181 |
information is stored: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
182 |
@{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>} |
28224 | 183 |
|
61406 | 184 |
\<^medskip> |
61575 | 185 |
Get the value only of the same settings variable, which is particularly |
186 |
useful in shell scripts: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
187 |
@{verbatim [display] \<open>isabelle getenv -b ISABELLE_OUTPUT\<close>} |
58618 | 188 |
\<close> |
28224 | 189 |
|
190 |
||
58618 | 191 |
section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close> |
28224 | 192 |
|
61575 | 193 |
text \<open> |
194 |
By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are |
|
195 |
just run from their location within the distribution directory, probably |
|
196 |
indirectly by the shell through its @{setting PATH}. Other schemes of |
|
197 |
installation are supported by the @{tool_def install} tool: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
198 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
199 |
\<open>Usage: isabelle install [OPTIONS] BINDIR |
28224 | 200 |
|
201 |
Options are: |
|
50132 | 202 |
-d DISTDIR refer to DISTDIR as Isabelle distribution |
28224 | 203 |
(default ISABELLE_HOME) |
204 |
||
50132 | 205 |
Install Isabelle executables with absolute references to the |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
206 |
distribution directory.\<close>} |
28224 | 207 |
|
61575 | 208 |
The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle distribution directory as |
209 |
determined by @{setting ISABELLE_HOME}. |
|
28224 | 210 |
|
61575 | 211 |
The \<open>BINDIR\<close> argument tells where executable wrapper scripts for |
212 |
@{executable "isabelle_process"} and @{executable isabelle} should be |
|
213 |
placed, which is typically a directory in the shell's @{setting PATH}, such |
|
214 |
as \<^verbatim>\<open>$HOME/bin\<close>. |
|
48815 | 215 |
|
61406 | 216 |
\<^medskip> |
61575 | 217 |
It is also possible to make symbolic links of the main Isabelle executables |
218 |
manually, but making separate copies outside the Isabelle distribution |
|
219 |
directory will not work! |
|
220 |
\<close> |
|
28224 | 221 |
|
222 |
||
58618 | 223 |
section \<open>Creating instances of the Isabelle logo\<close> |
28224 | 224 |
|
61575 | 225 |
text \<open> |
226 |
The @{tool_def logo} tool creates instances of the generic Isabelle logo as |
|
227 |
EPS and PDF, for inclusion in {\LaTeX} documents. |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
228 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
229 |
\<open>Usage: isabelle logo [OPTIONS] XYZ |
28224 | 230 |
|
49072
747835eb2782
"isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents:
48985
diff
changeset
|
231 |
Create instance XYZ of the Isabelle logo (as EPS and PDF). |
28224 | 232 |
|
233 |
Options are: |
|
49072
747835eb2782
"isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents:
48985
diff
changeset
|
234 |
-n NAME alternative output base name (default "isabelle_xyx") |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
235 |
-q quiet mode\<close>} |
48936 | 236 |
|
61575 | 237 |
Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the generated files. |
238 |
The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close> in lower-case. |
|
48936 | 239 |
|
61503 | 240 |
Option \<^verbatim>\<open>-q\<close> omits printing of the result file name. |
48936 | 241 |
|
61406 | 242 |
\<^medskip> |
61575 | 243 |
Implementors of Isabelle tools and applications are encouraged to make |
244 |
derived Isabelle logos for their own projects using this template. |
|
245 |
\<close> |
|
28224 | 246 |
|
247 |
||
58618 | 248 |
section \<open>Output the version identifier of the Isabelle distribution\<close> |
28224 | 249 |
|
58618 | 250 |
text \<open> |
48602 | 251 |
The @{tool_def version} tool displays Isabelle version information: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
252 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
253 |
\<open>Usage: isabelle version [OPTIONS] |
41511 | 254 |
|
255 |
Options are: |
|
256 |
-i short identification (derived from Mercurial id) |
|
257 |
||
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
258 |
Display Isabelle version information.\<close>} |
41511 | 259 |
|
61406 | 260 |
\<^medskip> |
61575 | 261 |
The default is to output the full version string of the Isabelle |
262 |
distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012: May 2012\<close>. |
|
41511 | 263 |
|
61575 | 264 |
The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial |
265 |
id of the @{setting ISABELLE_HOME} directory. |
|
58618 | 266 |
\<close> |
28224 | 267 |
|
268 |
||
58618 | 269 |
section \<open>Convert XML to YXML\<close> |
28224 | 270 |
|
58618 | 271 |
text \<open> |
61575 | 272 |
The @{tool_def yxml} tool converts a standard XML document (stdin) to the |
273 |
much simpler and more efficient YXML format of Isabelle (stdout). The YXML |
|
274 |
format is defined as follows. |
|
28224 | 275 |
|
61575 | 276 |
\<^enum> The encoding is always UTF-8. |
28224 | 277 |
|
61575 | 278 |
\<^enum> Body text is represented verbatim (no escaping, no special treatment of |
279 |
white space, no named entities, no CDATA chunks, no comments). |
|
28224 | 280 |
|
61575 | 281 |
\<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close> |
282 |
and \<open>\<^bold>Y = 6\<close> as follows: |
|
28224 | 283 |
|
61575 | 284 |
\begin{tabular}{ll} |
285 |
XML & YXML \\\hline |
|
286 |
\<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> & |
|
287 |
\<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\ |
|
288 |
\<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\ |
|
289 |
\end{tabular} |
|
28224 | 290 |
|
61575 | 291 |
There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated |
292 |
like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in |
|
293 |
well-formed XML documents. |
|
28224 | 294 |
|
295 |
Parsing YXML is pretty straight-forward: split the text into chunks |
|
61575 | 296 |
separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>. |
297 |
Markup chunks start with an empty sub-chunk, and a second empty sub-chunk |
|
298 |
indicates close of an element. Any other non-empty chunk consists of plain |
|
299 |
text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file |
|
300 |
"~~/src/Pure/PIDE/yxml.scala"}. |
|
28224 | 301 |
|
61575 | 302 |
YXML documents may be detected quickly by checking that the first two |
303 |
characters are \<open>\<^bold>X\<^bold>Y\<close>. |
|
58618 | 304 |
\<close> |
28224 | 305 |
|
306 |
end |