src/Doc/System/Environment.thy
 author wenzelm Wed Oct 04 12:00:53 2017 +0200 (19 months ago) changeset 66787 64b47495676d parent 66785 6fbd7fc824a9 child 66789 feb36b73a7f0 permissions -rw-r--r--
obsolete;
     1      (*:maxLineLen=78:*)

     2

     3 theory Environment

     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 \<^dir>\<open>$ISABELLE_HOME/bin\<close> files will not work!   48   49 \<^enum> The file \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> is run as a @{executable_ref

    50     bash} shell script with the auto-export option for variables enabled.

    51

    52     This file holds a rather long list of shell variable assignments, thus

    53     providing the site-wide default settings. The Isabelle distribution

    54     already contains a global settings file with sensible defaults for most

    55     variables. When installing the system, only a few of these may have to be

    56     adapted (probably @{setting ML_SYSTEM} etc.).

    57

    58     \<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it   59 exists) is run in the same way as the site default settings. Note that the   60 variable @{setting ISABELLE_HOME_USER} has already been set before ---   61 usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.

    62

    63     Thus individual users may override the site-wide defaults. Typically, a

    64     user settings file contains only a few lines, with some assignments that

    65     are actually changed. Never copy the central

    66     \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file!   67   68 Since settings files are regular GNU @{executable_def bash} scripts, one may   69 use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set   70 variables depending on the system architecture or other environment   71 variables. Such advanced features should be added only with great care,   72 though. In particular, external environment references should be kept at a   73 minimum.   74   75 \<^medskip>   76 A few variables are somewhat special:   77   78 \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path   79 name of the @{executable isabelle} executables.   80   81 \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle   82 distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\   83 @{setting ML_IDENTIFIER}) appended automatically to its value.   84   85 \<^medskip>   86 Note that the settings environment may be inspected with the @{tool getenv}   87 tool. This might help to figure out the effect of complex settings scripts.   88 \<close>   89   90   91 subsection \<open>Common variables\<close>   92   93 text \<open>   94 This is a reference of common Isabelle settings variables. Note that the   95 list is somewhat open-ended. Third-party utilities or interfaces may add   96 their own selection. Variables that are special in some sense are marked   97 with \<open>\<^sup>*\<close>.   98   99 \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory.   100 On Unix systems this is usually the same as @{setting HOME}, but on Windows   101 it is the regular home directory of the user, not the one of within the   102 Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its   103 HOME should point to the @{path "/home"} directory tree or the Windows user   104 home.\<close>   105   106 \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level   107 Isabelle distribution directory. This is automatically determined from the   108 Isabelle executable that has been invoked. Do not attempt to set @{setting   109 ISABELLE_HOME} yourself from the shell!   110   111 \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of   112 @{setting ISABELLE_HOME}. The default value is relative to @{path   113 "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the

   114   global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory

   115   mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide

   116   defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.   117   118 \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the   119 general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that   120 platform-dependent tools usually need to refer to the more specific   121 identification according to @{setting ISABELLE_PLATFORM}, @{setting   122 ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.   123   124 \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic   125 identifier for the underlying hardware and operating system. The Isabelle   126 platform identification always refers to the 32 bit variant, even this is a   127 64 bit machine. Note that the ML or Java runtime may have a different idea,   128 depending on which binaries are actually run.   129   130 \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting   131 ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform   132 that supports this; the value is empty for 32 bit. Note that the following   133 bash expression (including the quotes) prefers the 64 bit platform, if that   134 is available:   135   136 @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}   137   138 \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name   139 of the @{executable isabelle} executable.   140   141 \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this   142 Isabelle distribution, e.g.\ \<^verbatim>\<open>Isabelle2017\<close>''.   143   144 \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def   145 ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]   146 specify the underlying ML system to be used for Isabelle. There is only a   147 fixed set of admissable @{setting ML_SYSTEM} names (see the   148 \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution).

   149

   150   The actual compiler binary will be run from the directory @{setting

   151   ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.

   152   The optional @{setting ML_PLATFORM} may specify the binary format of ML heap

   153   images, which is useful for cross-platform installations. The value of

   154   @{setting ML_IDENTIFIER} is automatically obtained by composing the values

   155   of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version

   156   values.

   157

   158   \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java

   159   Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is

   160   essential for Isabelle/Scala and other JVM-based tools to work properly.

   161   Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime

   162   Environment), not JDK.

   163

   164   \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by

   165   colons) where Isabelle logic images may reside. When looking up heaps files,

   166   the value of @{setting ML_IDENTIFIER} is appended to each component

   167   internally.

   168

   169   \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files

   170   should be stored by default. The ML system and Isabelle version identifier

   171   is appended here, too.

   172

   173   \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory

   174   browser information is stored as HTML and PDF (see also \secref{sec:info}).

   175   The default value is @{path "$ISABELLE_HOME_USER/browser_info"}.   176   177 \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none   178 is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.   179   180 \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the   181 @{tool_ref console} interface.   182   183 \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},   184 @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle   185 document preparation (see also \secref{sec:tool-latex}).   186   187 \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories   188 that are scanned by @{executable isabelle} for external utility programs   189 (see also \secref{sec:isabelle-tool}).   190   191 \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories   192 with documentation files.   193   194 \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying   195 \<^verbatim>\<open>pdf\<close> files.   196   197 \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying   198 \<^verbatim>\<open>dvi\<close> files.   199   200 \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any   201 running Isabelle ML process derives an individual directory for temporary   202 files.   203 \<close>   204   205   206 subsection \<open>Additional components \label{sec:components}\<close>   207   208 text \<open>   209 Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The   210 general layout conventions are that of the main Isabelle distribution   211 itself, and the following two files (both optional) have a special meaning:   212   213 \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when   214 bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As   215 usual, the content is interpreted as a GNU bash script. It may refer to   216 the component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.   217   218 For example, the following setting allows to refer to files within the   219 component later on, without having to hardwire absolute paths:   220 @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}

   221

   222     Components can also add to existing Isabelle settings such as

   223     @{setting_def ISABELLE_TOOLS}, in order to provide component-specific

   224     tools that can be invoked by end-users. For example:

   225     @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}

   226

   227     \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same

   228     structure. The directory specifications given here can be either absolute

   229     (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory.

   230

   231   The root of component initialization is @{setting ISABELLE_HOME} itself.

   232   After initializing all of its sub-components recursively, @{setting

   233   ISABELLE_HOME_USER} is included in the same manner (if that directory

   234   exists). This allows to install private components via @{path

   235   "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient   236 to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the   237 \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component

   238   directory). For example: @{verbatim [display] \<open>init_component

   239   "$HOME/screwdriver-2.0"\<close>}   240   241 This is tolerant wrt.\ missing component directories, but might produce a   242 warning.   243   244 \<^medskip>   245 More complex situations may be addressed by initializing components listed   246 in a given catalog file, relatively to some base directory:   247 @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}

   248

   249   The component directories listed in the catalog file are treated as relative

   250   to the given base directory.

   251

   252   See also \secref{sec:tool-components} for some tool-support for resolving

   253   components that are formally initialized but not installed yet.

   254 \<close>

   255

   256

   257 section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>

   258

   259 text \<open>

   260   The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for

   261   Isabelle-related utilities, user interfaces, add-on applications etc. Such

   262   tools automatically benefit from the settings mechanism

   263   (\secref{sec:settings}). Moreover, this is the standard way to invoke

   264   Isabelle/Scala functionality as a separate operating-system process.

   265   Isabelle command-line tools are run uniformly via a common wrapper ---

   266   @{executable_ref isabelle}:

   267   @{verbatim [display]

   268 \<open>Usage: isabelle TOOL [ARGS ...]

   269

   270   Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.

   271

   272 Available tools:

   273   ...\<close>}

   274

   275   Tools may be implemented in Isabelle/Scala or as stand-alone executables

   276   (usually as GNU bash scripts). In the invocation of @{executable

   277   isabelle}~\<open>tool\<close>'', the named \<open>tool\<close> is resolved as follows (and in the

   278   given order).

   279

   280     \<^enum> An external tool found on the directories listed in the @{setting

   281     ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX

   282     notation).

   283

   284       \<^enum> If a file \<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the source needs to define

   285       some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. The Scala

   286       compiler is invoked on the spot (which may take some time), and the body

   287       function is run with the command-line arguments as \<^verbatim>\<open>List[String]\<close>.

   288

   289       \<^enum> If an executable file \<open>tool\<close>'' is found, it is invoked as

   290       stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close>

   291       array.

   292

   293     \<^enum> An internal tool that is registered in \<^verbatim>\<open>Isabelle_Tool.internal_tools\<close>

   294     within the Isabelle/Scala namespace of \<^verbatim>\<open>Pure.jar\<close>. This is the preferred

   295     entry-point for high-end tools implemented in Isabelle/Scala --- compiled

   296     once when the Isabelle distribution is built. These tools are provided by

   297     Isabelle/Pure and cannot be augmented in user-space.

   298

   299   There are also some administrative tools that are available from a bare

   300   repository clone of Isabelle, but not in regular distributions.

   301 \<close>

   302

   303

   304 subsubsection \<open>Examples\<close>

   305

   306 text \<open>

   307   Show the list of available documentation of the Isabelle distribution:

   308   @{verbatim [display] \<open>isabelle doc\<close>}

   309

   310   View a certain document as follows:

   311   @{verbatim [display] \<open>isabelle doc system\<close>}

   312

   313   Query the Isabelle settings environment:

   314   @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}

   315 \<close>

   316

   317

   318 section \<open>The raw Isabelle ML process\<close>

   319

   320 subsection \<open>Batch mode \label{sec:tool-process}\<close>

   321

   322 text \<open>

   323   The @{tool_def process} tool runs the raw ML process in batch mode:

   324   @{verbatim [display]

   325 \<open>Usage: isabelle process [OPTIONS]

   326

   327   Options are:

   328     -T THEORY    load theory

   329     -d DIR       include session directory

   330     -e ML_EXPR   evaluate ML expression on startup

   331     -f ML_FILE   evaluate ML file on startup

   332     -l NAME      logic session name (default ISABELLE_LOGIC="HOL")

   333     -m MODE      add print mode for output

   334     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)

   335

   336   Run the raw Isabelle ML process in batch mode.\<close>}

   337

   338   \<^medskip>

   339   Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is

   340   started. The source is either given literally or taken from a file. Multiple

   341   \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to

   342   premature exit of the ML process with return code 1.

   343

   344   \<^medskip>

   345   Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with

   346   a suitable @{ML use_thy} invocation.

   347

   348   \<^medskip>

   349   Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies

   350   additional directories for session roots, see also \secref{sec:tool-build}.

   351

   352   \<^medskip>

   353   The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this

   354   session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over

   355   mathematical Isabelle symbols.

   356

   357   \<^medskip>

   358   Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,

   359   see also \secref{sec:system-options}.

   360 \<close>

   361

   362

   363 subsubsection \<open>Example\<close>

   364

   365 text \<open>

   366   The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory

   367   loader within ML:

   368   @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}

   369

   370   Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The

   371   Isabelle/ML and Scala libraries provide functions for that, but here we need

   372   to do it manually.

   373 \<close>

   374

   375

   376 subsection \<open>Interactive mode\<close>

   377

   378 text \<open>

   379   The @{tool_def console} tool runs the raw ML process with interactive

   380   console and line editor:

   381   @{verbatim [display]

   382 \<open>Usage: isabelle console [OPTIONS]

   383

   384   Options are:

   385     -d DIR       include session directory

   386     -l NAME      logic session name (default ISABELLE_LOGIC)

   387     -m MODE      add print mode for output

   388     -n           no build of session image on startup

   389     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)

   390     -r           bootstrap from raw Poly/ML

   391     -s           system build mode for session image

   392

   393   Build a logic session image and run the raw Isabelle ML process

   394   in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}

   395

   396   \<^medskip>

   397   Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is

   398   checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.

   399

   400   Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is

   401   relevant for Isabelle/Pure development.

   402

   403   \<^medskip>

   404   Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}

   405   (\secref{sec:tool-process}).

   406

   407   Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build}

   408   (\secref{sec:tool-build}).

   409

   410   \<^medskip>

   411   The Isabelle/ML process is run through the line editor that is specified via

   412   the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\

   413   @{executable_def rlwrap} for GNU readline); the fall-back is to use plain

   414   standard input/output.

   415

   416   The user is connected to the raw ML toplevel loop: this is neither

   417   Isabelle/Isar nor Isabelle/ML within the usual formal context. The most

   418   relevant ML commands at this stage are @{ML use} (for ML files) and

   419   @{ML use_thy} (for theory files).

   420 \<close>

   421

   422

   423 section \<open>The raw Isabelle Java process \label{sec:isabelle-java}\<close>

   424

   425 text \<open>

   426   The @{executable_ref isabelle_java} executable allows to run a Java process

   427   within the name space of Java and Scala components that are bundled with

   428   Isabelle, but \<^emph>\<open>without\<close> the Isabelle settings environment

   429   (\secref{sec:settings}).

   430

   431   After such a JVM cold-start, the Isabelle environment can be accessed via

   432   \<^verbatim>\<open>Isabelle_System.getenv\<close> as usual, but the underlying process environment

   433   remains clean. This is e.g.\ relevant when invoking other processes that

   434   should remain separate from the current Isabelle installation.

   435

   436   \<^medskip>

   437   Note that under normal circumstances, Isabelle command-line tools are run

   438   \<^emph>\<open>within\<close> the settings environment, as provided by the @{executable

   439   isabelle} wrapper (\secref{sec:isabelle-tool} and \secref{sec:tool-java}).

   440 \<close>

   441

   442

   443 subsubsection \<open>Example\<close>

   444

   445 text \<open>

   446   The subsequent example creates a raw Java process on the command-line and

   447   invokes the main Isabelle application entry point:

   448   @{verbatim [display] \<open>isabelle_java isabelle.Main\<close>}

   449 \<close>

   450

   451

   452 section \<open>YXML versus XML\<close>

   453

   454 text \<open>

   455   Isabelle tools often use YXML, which is a simple and efficient syntax for

   456   untyped XML trees. The YXML format is defined as follows.

   457

   458     \<^enum> The encoding is always UTF-8.

   459

   460     \<^enum> Body text is represented verbatim (no escaping, no special treatment of

   461     white space, no named entities, no CDATA chunks, no comments).

   462

   463     \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>

   464     and \<open>\<^bold>Y = 6\<close> as follows:

   465

   466     \begin{tabular}{ll}

   467       XML & YXML \\\hline

   468       \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &

   469       \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\

   470       \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\

   471     \end{tabular}

   472

   473     There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated

   474     like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in

   475     well-formed XML documents.

   476

   477   Parsing YXML is pretty straight-forward: split the text into chunks

   478   separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.

   479   Markup chunks start with an empty sub-chunk, and a second empty sub-chunk

   480   indicates close of an element. Any other non-empty chunk consists of plain

   481   text. For example, see \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close> or

   482   \<^file>\<open>~~/src/Pure/PIDE/yxml.scala\<close>.

   483

   484   YXML documents may be detected quickly by checking that the first two

   485   characters are \<open>\<^bold>X\<^bold>Y\<close>.

   486 \<close>

   487

   488 end