1 (*:maxLineLen=78:*) |
|
2 |
|
3 theory Basics |
|
4 imports Base |
|
5 begin |
|
6 |
|
7 chapter \<open>The Isabelle system environment\<close> |
|
8 |
|
9 text \<open> |
|
10 This manual describes Isabelle together with related tools as seen from a |
|
11 system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite |
|
12 "isabelle-isar-ref"} for the actual Isabelle input language and related |
|
13 concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite |
|
14 "isabelle-implementation"} for the main concepts of the underlying |
|
15 implementation in Isabelle/ML. |
|
16 \<close> |
|
17 |
|
18 |
|
19 section \<open>Isabelle settings \label{sec:settings}\<close> |
|
20 |
|
21 text \<open> |
|
22 Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the |
|
23 process environment. This is a statically scoped collection of environment |
|
24 variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting |
|
25 ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the |
|
26 shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as |
|
27 explained below. |
|
28 \<close> |
|
29 |
|
30 |
|
31 subsection \<open>Bootstrapping the environment \label{sec:boot}\<close> |
|
32 |
|
33 text \<open> |
|
34 Isabelle executables need to be run within a proper settings environment. |
|
35 This is bootstrapped as described below, on the first invocation of one of |
|
36 the outer wrapper scripts (such as @{executable_ref isabelle}). This happens |
|
37 only once for each process tree, i.e.\ the environment is passed to |
|
38 subprocesses according to regular Unix conventions. |
|
39 |
|
40 \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined |
|
41 automatically from the location of the binary that has been run. |
|
42 |
|
43 You should not try to set @{setting ISABELLE_HOME} manually. Also note |
|
44 that the Isabelle executables either have to be run from their original |
|
45 location in the distribution directory, or via the executable objects |
|
46 created by the @{tool install} tool. Symbolic links are admissible, but a |
|
47 plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work! |
|
48 |
|
49 \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a |
|
50 @{executable_ref bash} shell script with the auto-export option for |
|
51 variables enabled. |
|
52 |
|
53 This file holds a rather long list of shell variable assignments, thus |
|
54 providing the site-wide default settings. The Isabelle distribution |
|
55 already contains a global settings file with sensible defaults for most |
|
56 variables. When installing the system, only a few of these may have to be |
|
57 adapted (probably @{setting ML_SYSTEM} etc.). |
|
58 |
|
59 \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it |
|
60 exists) is run in the same way as the site default settings. Note that the |
|
61 variable @{setting ISABELLE_HOME_USER} has already been set before --- |
|
62 usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>. |
|
63 |
|
64 Thus individual users may override the site-wide defaults. Typically, a |
|
65 user settings file contains only a few lines, with some assignments that |
|
66 are actually changed. Never copy the central @{file |
|
67 "$ISABELLE_HOME/etc/settings"} file! |
|
68 |
|
69 Since settings files are regular GNU @{executable_def bash} scripts, one may |
|
70 use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set |
|
71 variables depending on the system architecture or other environment |
|
72 variables. Such advanced features should be added only with great care, |
|
73 though. In particular, external environment references should be kept at a |
|
74 minimum. |
|
75 |
|
76 \<^medskip> |
|
77 A few variables are somewhat special: |
|
78 |
|
79 \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path |
|
80 name of the @{executable isabelle} executables. |
|
81 |
|
82 \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle |
|
83 distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\ |
|
84 @{setting ML_IDENTIFIER}) appended automatically to its value. |
|
85 |
|
86 \<^medskip> |
|
87 Note that the settings environment may be inspected with the @{tool getenv} |
|
88 tool. This might help to figure out the effect of complex settings scripts. |
|
89 \<close> |
|
90 |
|
91 |
|
92 subsection \<open>Common variables\<close> |
|
93 |
|
94 text \<open> |
|
95 This is a reference of common Isabelle settings variables. Note that the |
|
96 list is somewhat open-ended. Third-party utilities or interfaces may add |
|
97 their own selection. Variables that are special in some sense are marked |
|
98 with \<open>\<^sup>*\<close>. |
|
99 |
|
100 \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory. |
|
101 On Unix systems this is usually the same as @{setting HOME}, but on Windows |
|
102 it is the regular home directory of the user, not the one of within the |
|
103 Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its |
|
104 HOME should point to the @{file_unchecked "/home"} directory tree or the |
|
105 Windows user home.\<close> |
|
106 |
|
107 \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level |
|
108 Isabelle distribution directory. This is automatically determined from the |
|
109 Isabelle executable that has been invoked. Do not attempt to set @{setting |
|
110 ISABELLE_HOME} yourself from the shell! |
|
111 |
|
112 \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of |
|
113 @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked |
|
114 "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the |
|
115 global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory |
|
116 mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide |
|
117 defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. |
|
118 |
|
119 \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the |
|
120 general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that |
|
121 platform-dependent tools usually need to refer to the more specific |
|
122 identification according to @{setting ISABELLE_PLATFORM}, @{setting |
|
123 ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}. |
|
124 |
|
125 \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic |
|
126 identifier for the underlying hardware and operating system. The Isabelle |
|
127 platform identification always refers to the 32 bit variant, even this is a |
|
128 64 bit machine. Note that the ML or Java runtime may have a different idea, |
|
129 depending on which binaries are actually run. |
|
130 |
|
131 \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting |
|
132 ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform |
|
133 that supports this; the value is empty for 32 bit. Note that the following |
|
134 bash expression (including the quotes) prefers the 64 bit platform, if that |
|
135 is available: |
|
136 |
|
137 @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>} |
|
138 |
|
139 \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name |
|
140 of the @{executable isabelle} executable. Thus other tools and scripts need |
|
141 not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current |
|
142 search path of the shell. |
|
143 |
|
144 \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this |
|
145 Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''. |
|
146 |
|
147 \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def |
|
148 ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>] |
|
149 specify the underlying ML system to be used for Isabelle. There is only a |
|
150 fixed set of admissable @{setting ML_SYSTEM} names (see the @{file |
|
151 "$ISABELLE_HOME/etc/settings"} file of the distribution). |
|
152 |
|
153 The actual compiler binary will be run from the directory @{setting |
|
154 ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line. |
|
155 The optional @{setting ML_PLATFORM} may specify the binary format of ML heap |
|
156 images, which is useful for cross-platform installations. The value of |
|
157 @{setting ML_IDENTIFIER} is automatically obtained by composing the values |
|
158 of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version |
|
159 values. |
|
160 |
|
161 \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java |
|
162 Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is |
|
163 essential for Isabelle/Scala and other JVM-based tools to work properly. |
|
164 Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime |
|
165 Environment), not JDK. |
|
166 |
|
167 \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by |
|
168 colons) where Isabelle logic images may reside. When looking up heaps files, |
|
169 the value of @{setting ML_IDENTIFIER} is appended to each component |
|
170 internally. |
|
171 |
|
172 \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files |
|
173 should be stored by default. The ML system and Isabelle version identifier |
|
174 is appended here, too. |
|
175 |
|
176 \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory |
|
177 browser information is stored as HTML and PDF (see also \secref{sec:info}). |
|
178 The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}. |
|
179 |
|
180 \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none |
|
181 is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>. |
|
182 |
|
183 \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the |
|
184 @{tool_ref console} interface. |
|
185 |
|
186 \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX}, |
|
187 @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle |
|
188 document preparation (see also \secref{sec:tool-latex}). |
|
189 |
|
190 \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories |
|
191 that are scanned by @{executable isabelle} for external utility programs |
|
192 (see also \secref{sec:isabelle-tool}). |
|
193 |
|
194 \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories |
|
195 with documentation files. |
|
196 |
|
197 \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying |
|
198 \<^verbatim>\<open>pdf\<close> files. |
|
199 |
|
200 \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying |
|
201 \<^verbatim>\<open>dvi\<close> files. |
|
202 |
|
203 \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any |
|
204 running Isabelle ML process derives an individual directory for temporary |
|
205 files. |
|
206 \<close> |
|
207 |
|
208 |
|
209 subsection \<open>Additional components \label{sec:components}\<close> |
|
210 |
|
211 text \<open> |
|
212 Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The |
|
213 general layout conventions are that of the main Isabelle distribution |
|
214 itself, and the following two files (both optional) have a special meaning: |
|
215 |
|
216 \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when |
|
217 bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As |
|
218 usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the |
|
219 component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable. |
|
220 |
|
221 For example, the following setting allows to refer to files within the |
|
222 component later on, without having to hardwire absolute paths: |
|
223 @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>} |
|
224 |
|
225 Components can also add to existing Isabelle settings such as |
|
226 @{setting_def ISABELLE_TOOLS}, in order to provide component-specific |
|
227 tools that can be invoked by end-users. For example: |
|
228 @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>} |
|
229 |
|
230 \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same |
|
231 structure. The directory specifications given here can be either absolute |
|
232 (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory. |
|
233 |
|
234 The root of component initialization is @{setting ISABELLE_HOME} itself. |
|
235 After initializing all of its sub-components recursively, @{setting |
|
236 ISABELLE_HOME_USER} is included in the same manner (if that directory |
|
237 exists). This allows to install private components via @{file_unchecked |
|
238 "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient |
|
239 to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the |
|
240 \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component |
|
241 directory). For example: |
|
242 @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>} |
|
243 |
|
244 This is tolerant wrt.\ missing component directories, but might produce a |
|
245 warning. |
|
246 |
|
247 \<^medskip> |
|
248 More complex situations may be addressed by initializing components listed |
|
249 in a given catalog file, relatively to some base directory: |
|
250 @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>} |
|
251 |
|
252 The component directories listed in the catalog file are treated as relative |
|
253 to the given base directory. |
|
254 |
|
255 See also \secref{sec:tool-components} for some tool-support for resolving |
|
256 components that are formally initialized but not installed yet. |
|
257 \<close> |
|
258 |
|
259 |
|
260 section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close> |
|
261 |
|
262 text \<open> |
|
263 The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for |
|
264 Isabelle related utilities, user interfaces etc. Such tools automatically |
|
265 benefit from the settings mechanism. All Isabelle command-line tools are |
|
266 invoked via a common wrapper --- @{executable_ref isabelle}: |
|
267 @{verbatim [display] |
|
268 \<open>Usage: isabelle TOOL [ARGS ...] |
|
269 |
|
270 Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. |
|
271 |
|
272 Available tools: |
|
273 ...\<close>} |
|
274 |
|
275 In principle, Isabelle tools are ordinary executable scripts that are run |
|
276 within the Isabelle settings environment, see \secref{sec:settings}. The set |
|
277 of available tools is collected by @{executable isabelle} from the |
|
278 directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to |
|
279 call the scripts directly from the shell. Neither should you add the tool |
|
280 directories to your shell's search path! |
|
281 \<close> |
|
282 |
|
283 |
|
284 subsubsection \<open>Examples\<close> |
|
285 |
|
286 text \<open> |
|
287 Show the list of available documentation of the Isabelle distribution: |
|
288 @{verbatim [display] \<open>isabelle doc\<close>} |
|
289 |
|
290 View a certain document as follows: |
|
291 @{verbatim [display] \<open>isabelle doc system\<close>} |
|
292 |
|
293 Query the Isabelle settings environment: |
|
294 @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>} |
|
295 \<close> |
|
296 |
|
297 |
|
298 section \<open>The raw Isabelle ML process\<close> |
|
299 |
|
300 subsection \<open>Batch mode \label{sec:tool-process}\<close> |
|
301 |
|
302 text \<open> |
|
303 The @{tool_def process} tool runs the raw ML process in batch mode: |
|
304 @{verbatim [display] |
|
305 \<open>Usage: isabelle process [OPTIONS] |
|
306 |
|
307 Options are: |
|
308 -d DIR include session directory |
|
309 -e ML_EXPR evaluate ML expression on startup |
|
310 -f ML_FILE evaluate ML file on startup |
|
311 -l NAME logic session name (default ISABELLE_LOGIC="HOL") |
|
312 -m MODE add print mode for output |
|
313 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
314 |
|
315 Run the raw Isabelle ML process in batch mode.\<close>} |
|
316 \<close> |
|
317 |
|
318 |
|
319 subsubsection \<open>Options\<close> |
|
320 |
|
321 text \<open> |
|
322 Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is |
|
323 started. The source is either given literally or taken from a file. Multiple |
|
324 \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to |
|
325 premature exit of the ML process with return code 1. |
|
326 |
|
327 \<^medskip> |
|
328 Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies |
|
329 additional directories for session roots, see also \secref{sec:tool-build}. |
|
330 |
|
331 \<^medskip> |
|
332 The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this |
|
333 session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over |
|
334 mathematical Isabelle symbols. |
|
335 |
|
336 \<^medskip> |
|
337 Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process, |
|
338 see also \secref{sec:system-options}. |
|
339 \<close> |
|
340 |
|
341 |
|
342 subsubsection \<open>Example\<close> |
|
343 |
|
344 text \<open> |
|
345 The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory |
|
346 loader within ML: |
|
347 @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>} |
|
348 |
|
349 Observe the delicate quoting rules for the Bash shell vs.\ ML. The |
|
350 Isabelle/ML and Scala libraries provide functions for that, but here we need |
|
351 to do it manually. |
|
352 \<close> |
|
353 |
|
354 |
|
355 subsection \<open>Interactive mode\<close> |
|
356 |
|
357 text \<open> |
|
358 The @{tool_def console} tool runs the raw ML process with interactive |
|
359 console and line editor: |
|
360 @{verbatim [display] |
|
361 \<open>Usage: isabelle console [OPTIONS] |
|
362 |
|
363 Options are: |
|
364 -d DIR include session directory |
|
365 -l NAME logic session name (default ISABELLE_LOGIC) |
|
366 -m MODE add print mode for output |
|
367 -n no build of session image on startup |
|
368 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
369 -r logic session is RAW_ML_SYSTEM |
|
370 -s system build mode for session image |
|
371 |
|
372 Build a logic session image and run the raw Isabelle ML process |
|
373 in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>} |
|
374 |
|
375 Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is |
|
376 checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close> |
|
377 abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap |
|
378 Isabelle/Pure interactively. |
|
379 |
|
380 Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process} |
|
381 (\secref{sec:tool-process}). |
|
382 |
|
383 Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build} |
|
384 (\secref{sec:tool-build}). |
|
385 |
|
386 \<^medskip> |
|
387 The Isabelle/ML process is run through the line editor that is specified via |
|
388 the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\ |
|
389 @{executable_def rlwrap} for GNU readline); the fall-back is to use plain |
|
390 standard input/output. |
|
391 |
|
392 The user is connected to the raw ML toplevel loop: this is neither |
|
393 Isabelle/Isar nor Isabelle/ML within the usual formal context. The most |
|
394 relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML |
|
395 use_thys}. |
|
396 \<close> |
|
397 |
|
398 |
|
399 section \<open>YXML versus XML\<close> |
|
400 |
|
401 text \<open> |
|
402 Isabelle tools often use YXML, which is a simple and efficient syntax for |
|
403 untyped XML trees. The YXML format is defined as follows. |
|
404 |
|
405 \<^enum> The encoding is always UTF-8. |
|
406 |
|
407 \<^enum> Body text is represented verbatim (no escaping, no special treatment of |
|
408 white space, no named entities, no CDATA chunks, no comments). |
|
409 |
|
410 \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close> |
|
411 and \<open>\<^bold>Y = 6\<close> as follows: |
|
412 |
|
413 \begin{tabular}{ll} |
|
414 XML & YXML \\\hline |
|
415 \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> & |
|
416 \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\ |
|
417 \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\ |
|
418 \end{tabular} |
|
419 |
|
420 There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated |
|
421 like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in |
|
422 well-formed XML documents. |
|
423 |
|
424 Parsing YXML is pretty straight-forward: split the text into chunks |
|
425 separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>. |
|
426 Markup chunks start with an empty sub-chunk, and a second empty sub-chunk |
|
427 indicates close of an element. Any other non-empty chunk consists of plain |
|
428 text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file |
|
429 "~~/src/Pure/PIDE/yxml.scala"}. |
|
430 |
|
431 YXML documents may be detected quickly by checking that the first two |
|
432 characters are \<open>\<^bold>X\<^bold>Y\<close>. |
|
433 \<close> |
|
434 |
|
435 end |
|