src/Doc/System/Environment.thy
author wenzelm
Wed Oct 04 12:00:53 2017 +0200 (9 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