src/Doc/System/Environment.thy
author wenzelm
Sun, 20 Nov 2016 15:53:07 +0100
changeset 64509 80aaa4ff7fed
parent 63995 2e4d80723fb0
child 66732 e566fb4d43d4
child 66785 6fbd7fc824a9
permissions -rw-r--r--
documentation for Isabelle/Scala tools; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62640
diff changeset
     1
     (*:maxLineLen=78:*)
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
     2
62640
e36cbe677c17 clarified name;
wenzelm
parents: 62639
diff changeset
     3
theory Environment
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 41955
diff changeset
     4
imports Base
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     5
begin
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     6
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
     7
chapter \<open>The Isabelle system environment\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
     8
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
     9
text \<open>
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    10
  This manual describes Isabelle together with related tools as seen from a
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    11
  system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    12
  "isabelle-isar-ref"} for the actual Isabelle input language and related
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    13
  concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    14
  "isabelle-implementation"} for the main concepts of the underlying
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    15
  implementation in Isabelle/ML.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    16
\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    17
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    18
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    19
section \<open>Isabelle settings \label{sec:settings}\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    20
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    21
text \<open>
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    22
  Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    23
  process environment. This is a statically scoped collection of environment
62013
92a2372a226b discontinued documentation of old browser;
wenzelm
parents: 61656
diff changeset
    24
  variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
92a2372a226b discontinued documentation of old browser;
wenzelm
parents: 61656
diff changeset
    25
  ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    26
  shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    27
  explained below.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    28
\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    29
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    30
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    31
subsection \<open>Bootstrapping the environment \label{sec:boot}\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    32
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    33
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    34
  Isabelle executables need to be run within a proper settings environment.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    35
  This is bootstrapped as described below, on the first invocation of one of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    36
  the outer wrapper scripts (such as @{executable_ref isabelle}). This happens
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    37
  only once for each process tree, i.e.\ the environment is passed to
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    38
  subprocesses according to regular Unix conventions.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    39
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    40
    \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    41
    automatically from the location of the binary that has been run.
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    42
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    43
    You should not try to set @{setting ISABELLE_HOME} manually. Also note
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    44
    that the Isabelle executables either have to be run from their original
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    45
    location in the distribution directory, or via the executable objects
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    46
    created by the @{tool install} tool. Symbolic links are admissible, but a
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    47
    plain copy of the \<^dir>\<open>$ISABELLE_HOME/bin\<close> files will not work!
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    48
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    49
    \<^enum> The file \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> is run as a @{executable_ref
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    50
    bash} shell script with the auto-export option for variables enabled.
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
    51
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    52
    This file holds a rather long list of shell variable assignments, thus
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    53
    providing the site-wide default settings. The Isabelle distribution
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    54
    already contains a global settings file with sensible defaults for most
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    55
    variables. When installing the system, only a few of these may have to be
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    56
    adapted (probably @{setting ML_SYSTEM} etc.).
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    57
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62847
diff changeset
    58
    \<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    59
    exists) is run in the same way as the site default settings. Note that the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    60
    variable @{setting ISABELLE_HOME_USER} has already been set before ---
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    61
    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
61458
987533262fc2 Markdown support in document text;
wenzelm
parents: 61439
diff changeset
    62
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    63
    Thus individual users may override the site-wide defaults. Typically, a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    64
    user settings file contains only a few lines, with some assignments that
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    65
    are actually changed. Never copy the central
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    66
    \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file!
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    67
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    68
  Since settings files are regular GNU @{executable_def bash} scripts, one may
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    69
  use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    70
  variables depending on the system architecture or other environment
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    71
  variables. Such advanced features should be added only with great care,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    72
  though. In particular, external environment references should be kept at a
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    73
  minimum.
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    74
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 59904
diff changeset
    75
  \<^medskip>
eb2463fc4d7b more symbols;
wenzelm
parents: 59904
diff changeset
    76
  A few variables are somewhat special:
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    77
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    78
    \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
    79
    name of the @{executable isabelle} executables.
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    80
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    81
    \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    82
    distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    83
    @{setting ML_IDENTIFIER}) appended automatically to its value.
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    84
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 59904
diff changeset
    85
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    86
  Note that the settings environment may be inspected with the @{tool getenv}
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    87
  tool. This might help to figure out the effect of complex settings scripts.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    88
\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    89
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    90
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    91
subsection \<open>Common variables\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    92
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    93
text \<open>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    94
  This is a reference of common Isabelle settings variables. Note that the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    95
  list is somewhat open-ended. Third-party utilities or interfaces may add
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    96
  their own selection. Variables that are special in some sense are marked
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    97
  with \<open>\<^sup>*\<close>.
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
    98
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
    99
  \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   100
  On Unix systems this is usually the same as @{setting HOME}, but on Windows
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   101
  it is the regular home directory of the user, not the one of within the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   102
  Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62847
diff changeset
   103
  HOME should point to the @{path "/home"} directory tree or the Windows user
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62847
diff changeset
   104
  home.\<close>
47661
012a887997f3 USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents: 45028
diff changeset
   105
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   106
  \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   107
  Isabelle distribution directory. This is automatically determined from the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   108
  Isabelle executable that has been invoked. Do not attempt to set @{setting
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   109
  ISABELLE_HOME} yourself from the shell!
50182
30177ec0be36 added ISABELLE_PLATFORM_FAMILY;
wenzelm
parents: 49173
diff changeset
   110
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   111
  \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62847
diff changeset
   112
  @{setting ISABELLE_HOME}. The default value is relative to @{path
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   113
  "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   114
  global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   115
  mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   116
  defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   117
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   118
  \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   119
  general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
50182
30177ec0be36 added ISABELLE_PLATFORM_FAMILY;
wenzelm
parents: 49173
diff changeset
   120
  platform-dependent tools usually need to refer to the more specific
30177ec0be36 added ISABELLE_PLATFORM_FAMILY;
wenzelm
parents: 49173
diff changeset
   121
  identification according to @{setting ISABELLE_PLATFORM}, @{setting
30177ec0be36 added ISABELLE_PLATFORM_FAMILY;
wenzelm
parents: 49173
diff changeset
   122
  ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
30177ec0be36 added ISABELLE_PLATFORM_FAMILY;
wenzelm
parents: 49173
diff changeset
   123
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   124
  \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   125
  identifier for the underlying hardware and operating system. The Isabelle
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   126
  platform identification always refers to the 32 bit variant, even this is a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   127
  64 bit machine. Note that the ML or Java runtime may have a different idea,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   128
  depending on which binaries are actually run.
36196
cbb9ee265cdd added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents: 33952
diff changeset
   129
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   130
  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   131
  ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   132
  that supports this; the value is empty for 32 bit. Note that the following
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   133
  bash expression (including the quotes) prefers the 64 bit platform, if that
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   134
  is available:
47823
4fad76e6f4ba some manual updates;
wenzelm
parents: 47661
diff changeset
   135
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   136
  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
36196
cbb9ee265cdd added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents: 33952
diff changeset
   137
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   138
  \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   139
  of the @{executable isabelle} executable. Thus other tools and scripts need
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   140
  not assume that the \<^dir>\<open>$ISABELLE_HOME/bin\<close> directory is on the current
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   141
  search path of the shell.
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   142
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   143
  \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   144
  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   145
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   146
  \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   147
  ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   148
  specify the underlying ML system to be used for Isabelle. There is only a
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   149
  fixed set of admissable @{setting ML_SYSTEM} names (see the
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   150
  \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution).
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   151
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   152
  The actual compiler binary will be run from the directory @{setting
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   153
  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   154
  The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   155
  images, which is useful for cross-platform installations. The value of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   156
  @{setting ML_IDENTIFIER} is automatically obtained by composing the values
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   157
  of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   158
  values.
47823
4fad76e6f4ba some manual updates;
wenzelm
parents: 47661
diff changeset
   159
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   160
  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   161
  Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   162
  essential for Isabelle/Scala and other JVM-based tools to work properly.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   163
  Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
47823
4fad76e6f4ba some manual updates;
wenzelm
parents: 47661
diff changeset
   164
  Environment), not JDK.
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   165
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   166
  \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   167
  colons) where Isabelle logic images may reside. When looking up heaps files,
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   168
  the value of @{setting ML_IDENTIFIER} is appended to each component
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   169
  internally.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   170
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   171
  \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   172
  should be stored by default. The ML system and Isabelle version identifier
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   173
  is appended here, too.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   174
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   175
  \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
62013
92a2372a226b discontinued documentation of old browser;
wenzelm
parents: 61656
diff changeset
   176
  browser information is stored as HTML and PDF (see also \secref{sec:info}).
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62847
diff changeset
   177
  The default value is @{path "$ISABELLE_HOME_USER/browser_info"}.
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   178
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   179
  \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   180
  is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   181
62562
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
   182
  \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
   183
  @{tool_ref console} interface.
905a5db3932d back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents: 62559
diff changeset
   184
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   185
  \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   186
  @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   187
  document preparation (see also \secref{sec:tool-latex}).
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   188
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   189
  \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   190
  that are scanned by @{executable isabelle} for external utility programs
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   191
  (see also \secref{sec:isabelle-tool}).
50197
b385d134926d eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;
wenzelm
parents: 50182
diff changeset
   192
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   193
  \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   194
  with documentation files.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   195
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   196
  \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   197
  \<^verbatim>\<open>pdf\<close> files.
54683
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 52746
diff changeset
   198
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   199
  \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   200
  \<^verbatim>\<open>dvi\<close> files.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   201
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   202
  \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   203
  running Isabelle ML process derives an individual directory for temporary
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   204
  files.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   205
\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   206
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   207
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   208
subsection \<open>Additional components \label{sec:components}\<close>
32323
8185d3bfcbf1 tuned "Bootstrapping the environment";
wenzelm
parents: 32088
diff changeset
   209
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   210
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   211
  Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   212
  general layout conventions are that of the main Isabelle distribution
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   213
  itself, and the following two files (both optional) have a special meaning:
32323
8185d3bfcbf1 tuned "Bootstrapping the environment";
wenzelm
parents: 32088
diff changeset
   214
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   215
    \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   216
    bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
64509
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   217
    usual, the content is interpreted as a GNU bash script. It may refer to
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   218
    the component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
32323
8185d3bfcbf1 tuned "Bootstrapping the environment";
wenzelm
parents: 32088
diff changeset
   219
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   220
    For example, the following setting allows to refer to files within the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   221
    component later on, without having to hardwire absolute paths:
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   222
    @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
32323
8185d3bfcbf1 tuned "Bootstrapping the environment";
wenzelm
parents: 32088
diff changeset
   223
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   224
    Components can also add to existing Isabelle settings such as
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   225
    @{setting_def ISABELLE_TOOLS}, in order to provide component-specific
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   226
    tools that can be invoked by end-users. For example:
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   227
    @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
32323
8185d3bfcbf1 tuned "Bootstrapping the environment";
wenzelm
parents: 32088
diff changeset
   228
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   229
    \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   230
    structure. The directory specifications given here can be either absolute
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   231
    (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory.
32323
8185d3bfcbf1 tuned "Bootstrapping the environment";
wenzelm
parents: 32088
diff changeset
   232
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   233
  The root of component initialization is @{setting ISABELLE_HOME} itself.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   234
  After initializing all of its sub-components recursively, @{setting
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   235
  ISABELLE_HOME_USER} is included in the same manner (if that directory
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62847
diff changeset
   236
  exists). This allows to install private components via @{path
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   237
  "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   238
  to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   239
  \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62847
diff changeset
   240
  directory). For example: @{verbatim [display] \<open>init_component
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62847
diff changeset
   241
  "$HOME/screwdriver-2.0"\<close>}
48838
623ba165d059 direct support for component forests via init_components;
wenzelm
parents: 48813
diff changeset
   242
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   243
  This is tolerant wrt.\ missing component directories, but might produce a
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   244
  warning.
48838
623ba165d059 direct support for component forests via init_components;
wenzelm
parents: 48813
diff changeset
   245
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 59904
diff changeset
   246
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   247
  More complex situations may be addressed by initializing components listed
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   248
  in a given catalog file, relatively to some base directory:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   249
  @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}
48838
623ba165d059 direct support for component forests via init_components;
wenzelm
parents: 48813
diff changeset
   250
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   251
  The component directories listed in the catalog file are treated as relative
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   252
  to the given base directory.
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48838
diff changeset
   253
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   254
  See also \secref{sec:tool-components} for some tool-support for resolving
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   255
  components that are formally initialized but not installed yet.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   256
\<close>
32323
8185d3bfcbf1 tuned "Bootstrapping the environment";
wenzelm
parents: 32088
diff changeset
   257
8185d3bfcbf1 tuned "Bootstrapping the environment";
wenzelm
parents: 32088
diff changeset
   258
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   259
section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   260
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   261
text \<open>
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   262
  The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
64509
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   263
  Isabelle-related utilities, user interfaces, add-on applications etc. Such
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   264
  tools automatically benefit from the settings mechanism
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   265
  (\secref{sec:settings}). Moreover, this is the standard way to invoke
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   266
  Isabelle/Scala functionality as a separate operating-system process.
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   267
  Isabelle command-line tools are run uniformly via a common wrapper ---
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   268
  @{executable_ref isabelle}:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   269
  @{verbatim [display]
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   270
\<open>Usage: isabelle TOOL [ARGS ...]
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   271
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62677
diff changeset
   272
  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   273
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   274
Available tools:
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   275
  ...\<close>}
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   276
64509
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   277
  Tools may be implemented in Isabelle/Scala or as stand-alone executables
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   278
  (usually as GNU bash scripts). In the invocation of ``@{executable
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   279
  isabelle}~\<open>tool\<close>'', the named \<open>tool\<close> is resolved as follows (and in the
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   280
  given order).
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   281
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   282
    \<^enum> An external tool found on the directories listed in the @{setting
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   283
    ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   284
    notation).
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   285
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   286
      \<^enum> If a file ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the source needs to define
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   287
      some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. The Scala
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   288
      compiler is invoked on the spot (which may take some time), and the body
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   289
      function is run with the command-line arguments as \<^verbatim>\<open>List[String]\<close>.
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   290
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   291
      \<^enum> If an executable file ``\<open>tool\<close>'' is found, it is invoked as
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   292
      stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close>
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   293
      array.
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   294
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   295
    \<^enum> An internal tool that is registered in \<^verbatim>\<open>Isabelle_Tool.internal_tools\<close>
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   296
    within the Isabelle/Scala namespace of \<^verbatim>\<open>Pure.jar\<close>. This is the preferred
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   297
    entry-point for high-end tools implemented in Isabelle/Scala --- compiled
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   298
    once when the Isabelle distribution is built. These tools are provided by
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   299
    Isabelle/Pure and cannot be augmented in user-space.
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   300
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   301
  There are also some administrative tools that are available from a bare
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   302
  repository clone of Isabelle, but not in regular distributions.
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   303
\<close>
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   304
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   305
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   306
subsubsection \<open>Examples\<close>
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   307
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   308
text \<open>
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   309
  Show the list of available documentation of the Isabelle distribution:
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   310
  @{verbatim [display] \<open>isabelle doc\<close>}
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   311
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   312
  View a certain document as follows:
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   313
  @{verbatim [display] \<open>isabelle doc system\<close>}
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   314
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   315
  Query the Isabelle settings environment:
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   316
  @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   317
\<close>
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   318
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   319
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   320
section \<open>The raw Isabelle ML process\<close>
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   321
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   322
subsection \<open>Batch mode \label{sec:tool-process}\<close>
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   323
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   324
text \<open>
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   325
  The @{tool_def process} tool runs the raw ML process in batch mode:
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   326
  @{verbatim [display]
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62588
diff changeset
   327
\<open>Usage: isabelle process [OPTIONS]
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   328
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   329
  Options are:
62677
0df43889f496 isabelle process -T THEORY;
wenzelm
parents: 62643
diff changeset
   330
    -T THEORY    load theory
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62634
diff changeset
   331
    -d DIR       include session directory
62506
860cd901ab43 clarified isabelle_process;
wenzelm
parents: 62475
diff changeset
   332
    -e ML_EXPR   evaluate ML expression on startup
860cd901ab43 clarified isabelle_process;
wenzelm
parents: 62475
diff changeset
   333
    -f ML_FILE   evaluate ML file on startup
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62588
diff changeset
   334
    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   335
    -m MODE      add print mode for output
52056
fc458f304f93 added isabelle-process option -o;
wenzelm
parents: 52054
diff changeset
   336
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   337
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62588
diff changeset
   338
  Run the raw Isabelle ML process in batch mode.\<close>}
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   339
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62640
diff changeset
   340
  \<^medskip>
62506
860cd901ab43 clarified isabelle_process;
wenzelm
parents: 62475
diff changeset
   341
  Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
860cd901ab43 clarified isabelle_process;
wenzelm
parents: 62475
diff changeset
   342
  started. The source is either given literally or taken from a file. Multiple
860cd901ab43 clarified isabelle_process;
wenzelm
parents: 62475
diff changeset
   343
  \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
860cd901ab43 clarified isabelle_process;
wenzelm
parents: 62475
diff changeset
   344
  premature exit of the ML process with return code 1.
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   345
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 59904
diff changeset
   346
  \<^medskip>
62677
0df43889f496 isabelle process -T THEORY;
wenzelm
parents: 62643
diff changeset
   347
  Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with
0df43889f496 isabelle process -T THEORY;
wenzelm
parents: 62643
diff changeset
   348
  a suitable @{ML use_thy} invocation.
0df43889f496 isabelle process -T THEORY;
wenzelm
parents: 62643
diff changeset
   349
0df43889f496 isabelle process -T THEORY;
wenzelm
parents: 62643
diff changeset
   350
  \<^medskip>
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62634
diff changeset
   351
  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies
699e86051e35 isabelle process -d;
wenzelm
parents: 62634
diff changeset
   352
  additional directories for session roots, see also \secref{sec:tool-build}.
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62588
diff changeset
   353
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62588
diff changeset
   354
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   355
  The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62562
diff changeset
   356
  session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62562
diff changeset
   357
  mathematical Isabelle symbols.
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   358
61406
eb2463fc4d7b more symbols;
wenzelm
parents: 59904
diff changeset
   359
  \<^medskip>
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61572
diff changeset
   360
  Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62562
diff changeset
   361
  see also \secref{sec:system-options}.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   362
\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   363
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   364
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   365
subsubsection \<open>Example\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   366
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   367
text \<open>
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   368
  The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   369
  loader within ML:
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62588
diff changeset
   370
  @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   371
64509
80aaa4ff7fed documentation for Isabelle/Scala tools;
wenzelm
parents: 63995
diff changeset
   372
  Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   373
  Isabelle/ML and Scala libraries provide functions for that, but here we need
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   374
  to do it manually.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   375
\<close>
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
   376
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
   377
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   378
subsection \<open>Interactive mode\<close>
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
   379
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   380
text \<open>
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   381
  The @{tool_def console} tool runs the raw ML process with interactive
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   382
  console and line editor:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61406
diff changeset
   383
  @{verbatim [display]
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   384
\<open>Usage: isabelle console [OPTIONS]
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
   385
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   386
  Options are:
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   387
    -d DIR       include session directory
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   388
    -l NAME      logic session name (default ISABELLE_LOGIC)
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   389
    -m MODE      add print mode for output
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   390
    -n           no build of session image on startup
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   391
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62640
diff changeset
   392
    -r           bootstrap from raw Poly/ML
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   393
    -s           system build mode for session image
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
   394
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   395
  Build a logic session image and run the raw Isabelle ML process
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   396
  in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
   397
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62640
diff changeset
   398
  \<^medskip>
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   399
  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62640
diff changeset
   400
  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
   401
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62640
diff changeset
   402
  Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62640
diff changeset
   403
  relevant for Isabelle/Pure development.
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62640
diff changeset
   404
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62640
diff changeset
   405
  \<^medskip>
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62634
diff changeset
   406
  Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
699e86051e35 isabelle process -d;
wenzelm
parents: 62634
diff changeset
   407
  (\secref{sec:tool-process}).
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   408
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62634
diff changeset
   409
  Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build}
699e86051e35 isabelle process -d;
wenzelm
parents: 62634
diff changeset
   410
  (\secref{sec:tool-build}).
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
   411
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   412
  \<^medskip>
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   413
  The Isabelle/ML process is run through the line editor that is specified via
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   414
  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   415
  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   416
  standard input/output.
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28223
diff changeset
   417
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   418
  The user is connected to the raw ML toplevel loop: this is neither
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62576
diff changeset
   419
  Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
62847
1bd1d8492931 clarified bootstrap;
wenzelm
parents: 62829
diff changeset
   420
  relevant ML commands at this stage are @{ML use} (for ML files) and
1bd1d8492931 clarified bootstrap;
wenzelm
parents: 62829
diff changeset
   421
  @{ML use_thy} (for theory files).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
   422
\<close>
28215
a1cfc43ac47d converted basics.tex to theory file;
wenzelm
parents:
diff changeset
   423
62451
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   424
63995
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   425
section \<open>The raw Isabelle Java process \label{sec:isabelle-java}\<close>
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   426
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   427
text \<open>
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   428
  The @{executable_ref isabelle_java} executable allows to run a Java process
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   429
  within the name space of Java and Scala components that are bundled with
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   430
  Isabelle, but \<^emph>\<open>without\<close> the Isabelle settings environment
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   431
  (\secref{sec:settings}).
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   432
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   433
  After such a JVM cold-start, the Isabelle environment can be accessed via
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   434
  \<^verbatim>\<open>Isabelle_System.getenv\<close> as usual, but the underlying process environment
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   435
  remains clean. This is e.g.\ relevant when invoking other processes that
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   436
  should remain separate from the current Isabelle installation.
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   437
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   438
  \<^medskip>
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   439
  Note that under normal circumstances, Isabelle command-line tools are run
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   440
  \<^emph>\<open>within\<close> the settings environment, as provided by the @{executable
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   441
  isabelle} wrapper (\secref{sec:isabelle-tool} and \secref{sec:tool-java}).
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   442
\<close>
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   443
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   444
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   445
subsubsection \<open>Example\<close>
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   446
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   447
text \<open>
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   448
  The subsequent example creates a raw Java process on the command-line and
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   449
  invokes the main Isabelle application entry point:
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   450
  @{verbatim [display] \<open>isabelle_java isabelle.Main\<close>}
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   451
\<close>
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   452
2e4d80723fb0 added isabelle_java cold-start executable;
wenzelm
parents: 63680
diff changeset
   453
62451
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   454
section \<open>YXML versus XML\<close>
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   455
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   456
text \<open>
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   457
  Isabelle tools often use YXML, which is a simple and efficient syntax for
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   458
  untyped XML trees. The YXML format is defined as follows.
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   459
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   460
    \<^enum> The encoding is always UTF-8.
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   461
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   462
    \<^enum> Body text is represented verbatim (no escaping, no special treatment of
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   463
    white space, no named entities, no CDATA chunks, no comments).
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   464
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   465
    \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   466
    and \<open>\<^bold>Y = 6\<close> as follows:
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   467
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   468
    \begin{tabular}{ll}
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   469
      XML & YXML \\\hline
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   470
      \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   471
      \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   472
      \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   473
    \end{tabular}
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   474
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   475
    There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   476
    like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   477
    well-formed XML documents.
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   478
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   479
  Parsing YXML is pretty straight-forward: split the text into chunks
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   480
  separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   481
  Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   482
  indicates close of an element. Any other non-empty chunk consists of plain
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   483
  text. For example, see \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close> or
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   484
  \<^file>\<open>~~/src/Pure/PIDE/yxml.scala\<close>.
62451
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   485
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   486
  YXML documents may be detected quickly by checking that the first two
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   487
  characters are \<open>\<^bold>X\<^bold>Y\<close>.
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   488
\<close>
040b94ffbdde removed pointless "isabelle yxml";
wenzelm
parents: 62354
diff changeset
   489
28223
wenzelm
parents: 28215
diff changeset
   490
end