clarified name;
authorwenzelm
Wed Mar 16 21:14:59 2016 +0100 (2016-03-16)
changeset 62640e36cbe677c17
parent 62639 699e86051e35
child 62641 0b1b7465f2ef
clarified name;
src/Doc/ROOT
src/Doc/System/Basics.thy
src/Doc/System/Environment.thy
src/Doc/System/document/root.tex
     1.1 --- a/src/Doc/ROOT	Wed Mar 16 21:11:15 2016 +0100
     1.2 +++ b/src/Doc/ROOT	Wed Mar 16 21:14:59 2016 +0100
     1.3 @@ -357,7 +357,7 @@
     1.4  session System (doc) in "System" = Pure +
     1.5    options [document_variants = "system", thy_output_source]
     1.6    theories
     1.7 -    Basics
     1.8 +    Environment
     1.9      Sessions
    1.10      Presentation
    1.11      Scala
     2.1 --- a/src/Doc/System/Basics.thy	Wed Mar 16 21:11:15 2016 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,435 +0,0 @@
     2.4 -(*:maxLineLen=78:*)
     2.5 -
     2.6 -theory Basics
     2.7 -imports Base
     2.8 -begin
     2.9 -
    2.10 -chapter \<open>The Isabelle system environment\<close>
    2.11 -
    2.12 -text \<open>
    2.13 -  This manual describes Isabelle together with related tools as seen from a
    2.14 -  system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
    2.15 -  "isabelle-isar-ref"} for the actual Isabelle input language and related
    2.16 -  concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
    2.17 -  "isabelle-implementation"} for the main concepts of the underlying
    2.18 -  implementation in Isabelle/ML.
    2.19 -\<close>
    2.20 -
    2.21 -
    2.22 -section \<open>Isabelle settings \label{sec:settings}\<close>
    2.23 -
    2.24 -text \<open>
    2.25 -  Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the
    2.26 -  process environment. This is a statically scoped collection of environment
    2.27 -  variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
    2.28 -  ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
    2.29 -  shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
    2.30 -  explained below.
    2.31 -\<close>
    2.32 -
    2.33 -
    2.34 -subsection \<open>Bootstrapping the environment \label{sec:boot}\<close>
    2.35 -
    2.36 -text \<open>
    2.37 -  Isabelle executables need to be run within a proper settings environment.
    2.38 -  This is bootstrapped as described below, on the first invocation of one of
    2.39 -  the outer wrapper scripts (such as @{executable_ref isabelle}). This happens
    2.40 -  only once for each process tree, i.e.\ the environment is passed to
    2.41 -  subprocesses according to regular Unix conventions.
    2.42 -
    2.43 -    \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined
    2.44 -    automatically from the location of the binary that has been run.
    2.45 -
    2.46 -    You should not try to set @{setting ISABELLE_HOME} manually. Also note
    2.47 -    that the Isabelle executables either have to be run from their original
    2.48 -    location in the distribution directory, or via the executable objects
    2.49 -    created by the @{tool install} tool. Symbolic links are admissible, but a
    2.50 -    plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work!
    2.51 -
    2.52 -    \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
    2.53 -    @{executable_ref bash} shell script with the auto-export option for
    2.54 -    variables enabled.
    2.55 -
    2.56 -    This file holds a rather long list of shell variable assignments, thus
    2.57 -    providing the site-wide default settings. The Isabelle distribution
    2.58 -    already contains a global settings file with sensible defaults for most
    2.59 -    variables. When installing the system, only a few of these may have to be
    2.60 -    adapted (probably @{setting ML_SYSTEM} etc.).
    2.61 -
    2.62 -    \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
    2.63 -    exists) is run in the same way as the site default settings. Note that the
    2.64 -    variable @{setting ISABELLE_HOME_USER} has already been set before ---
    2.65 -    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
    2.66 -
    2.67 -    Thus individual users may override the site-wide defaults. Typically, a
    2.68 -    user settings file contains only a few lines, with some assignments that
    2.69 -    are actually changed. Never copy the central @{file
    2.70 -    "$ISABELLE_HOME/etc/settings"} file!
    2.71 -
    2.72 -  Since settings files are regular GNU @{executable_def bash} scripts, one may
    2.73 -  use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
    2.74 -  variables depending on the system architecture or other environment
    2.75 -  variables. Such advanced features should be added only with great care,
    2.76 -  though. In particular, external environment references should be kept at a
    2.77 -  minimum.
    2.78 -
    2.79 -  \<^medskip>
    2.80 -  A few variables are somewhat special:
    2.81 -
    2.82 -    \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
    2.83 -    name of the @{executable isabelle} executables.
    2.84 -
    2.85 -    \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
    2.86 -    distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
    2.87 -    @{setting ML_IDENTIFIER}) appended automatically to its value.
    2.88 -
    2.89 -  \<^medskip>
    2.90 -  Note that the settings environment may be inspected with the @{tool getenv}
    2.91 -  tool. This might help to figure out the effect of complex settings scripts.
    2.92 -\<close>
    2.93 -
    2.94 -
    2.95 -subsection \<open>Common variables\<close>
    2.96 -
    2.97 -text \<open>
    2.98 -  This is a reference of common Isabelle settings variables. Note that the
    2.99 -  list is somewhat open-ended. Third-party utilities or interfaces may add
   2.100 -  their own selection. Variables that are special in some sense are marked
   2.101 -  with \<open>\<^sup>*\<close>.
   2.102 -
   2.103 -  \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory.
   2.104 -  On Unix systems this is usually the same as @{setting HOME}, but on Windows
   2.105 -  it is the regular home directory of the user, not the one of within the
   2.106 -  Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
   2.107 -  HOME should point to the @{file_unchecked "/home"} directory tree or the
   2.108 -  Windows user home.\<close>
   2.109 -
   2.110 -  \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
   2.111 -  Isabelle distribution directory. This is automatically determined from the
   2.112 -  Isabelle executable that has been invoked. Do not attempt to set @{setting
   2.113 -  ISABELLE_HOME} yourself from the shell!
   2.114 -
   2.115 -  \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
   2.116 -  @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked
   2.117 -  "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
   2.118 -  global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
   2.119 -  mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
   2.120 -  defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
   2.121 -
   2.122 -  \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
   2.123 -  general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
   2.124 -  platform-dependent tools usually need to refer to the more specific
   2.125 -  identification according to @{setting ISABELLE_PLATFORM}, @{setting
   2.126 -  ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
   2.127 -
   2.128 -  \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
   2.129 -  identifier for the underlying hardware and operating system. The Isabelle
   2.130 -  platform identification always refers to the 32 bit variant, even this is a
   2.131 -  64 bit machine. Note that the ML or Java runtime may have a different idea,
   2.132 -  depending on which binaries are actually run.
   2.133 -
   2.134 -  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
   2.135 -  ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
   2.136 -  that supports this; the value is empty for 32 bit. Note that the following
   2.137 -  bash expression (including the quotes) prefers the 64 bit platform, if that
   2.138 -  is available:
   2.139 -
   2.140 -  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
   2.141 -
   2.142 -  \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
   2.143 -  of the @{executable isabelle} executable. Thus other tools and scripts need
   2.144 -  not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current
   2.145 -  search path of the shell.
   2.146 -
   2.147 -  \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
   2.148 -  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
   2.149 -
   2.150 -  \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
   2.151 -  ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
   2.152 -  specify the underlying ML system to be used for Isabelle. There is only a
   2.153 -  fixed set of admissable @{setting ML_SYSTEM} names (see the @{file
   2.154 -  "$ISABELLE_HOME/etc/settings"} file of the distribution).
   2.155 -
   2.156 -  The actual compiler binary will be run from the directory @{setting
   2.157 -  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
   2.158 -  The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
   2.159 -  images, which is useful for cross-platform installations. The value of
   2.160 -  @{setting ML_IDENTIFIER} is automatically obtained by composing the values
   2.161 -  of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
   2.162 -  values.
   2.163 -
   2.164 -  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
   2.165 -  Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
   2.166 -  essential for Isabelle/Scala and other JVM-based tools to work properly.
   2.167 -  Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
   2.168 -  Environment), not JDK.
   2.169 -
   2.170 -  \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
   2.171 -  colons) where Isabelle logic images may reside. When looking up heaps files,
   2.172 -  the value of @{setting ML_IDENTIFIER} is appended to each component
   2.173 -  internally.
   2.174 -
   2.175 -  \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
   2.176 -  should be stored by default. The ML system and Isabelle version identifier
   2.177 -  is appended here, too.
   2.178 -
   2.179 -  \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
   2.180 -  browser information is stored as HTML and PDF (see also \secref{sec:info}).
   2.181 -  The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
   2.182 -
   2.183 -  \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
   2.184 -  is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
   2.185 -
   2.186 -  \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
   2.187 -  @{tool_ref console} interface.
   2.188 -
   2.189 -  \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
   2.190 -  @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
   2.191 -  document preparation (see also \secref{sec:tool-latex}).
   2.192 -
   2.193 -  \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
   2.194 -  that are scanned by @{executable isabelle} for external utility programs
   2.195 -  (see also \secref{sec:isabelle-tool}).
   2.196 -
   2.197 -  \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories
   2.198 -  with documentation files.
   2.199 -
   2.200 -  \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
   2.201 -  \<^verbatim>\<open>pdf\<close> files.
   2.202 -
   2.203 -  \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying
   2.204 -  \<^verbatim>\<open>dvi\<close> files.
   2.205 -
   2.206 -  \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
   2.207 -  running Isabelle ML process derives an individual directory for temporary
   2.208 -  files.
   2.209 -\<close>
   2.210 -
   2.211 -
   2.212 -subsection \<open>Additional components \label{sec:components}\<close>
   2.213 -
   2.214 -text \<open>
   2.215 -  Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The
   2.216 -  general layout conventions are that of the main Isabelle distribution
   2.217 -  itself, and the following two files (both optional) have a special meaning:
   2.218 -
   2.219 -    \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
   2.220 -    bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
   2.221 -    usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the
   2.222 -    component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
   2.223 -
   2.224 -    For example, the following setting allows to refer to files within the
   2.225 -    component later on, without having to hardwire absolute paths:
   2.226 -    @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
   2.227 -
   2.228 -    Components can also add to existing Isabelle settings such as
   2.229 -    @{setting_def ISABELLE_TOOLS}, in order to provide component-specific
   2.230 -    tools that can be invoked by end-users. For example:
   2.231 -    @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
   2.232 -
   2.233 -    \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same
   2.234 -    structure. The directory specifications given here can be either absolute
   2.235 -    (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory.
   2.236 -
   2.237 -  The root of component initialization is @{setting ISABELLE_HOME} itself.
   2.238 -  After initializing all of its sub-components recursively, @{setting
   2.239 -  ISABELLE_HOME_USER} is included in the same manner (if that directory
   2.240 -  exists). This allows to install private components via @{file_unchecked
   2.241 -  "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
   2.242 -  to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
   2.243 -  \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
   2.244 -  directory). For example:
   2.245 -  @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
   2.246 -
   2.247 -  This is tolerant wrt.\ missing component directories, but might produce a
   2.248 -  warning.
   2.249 -
   2.250 -  \<^medskip>
   2.251 -  More complex situations may be addressed by initializing components listed
   2.252 -  in a given catalog file, relatively to some base directory:
   2.253 -  @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}
   2.254 -
   2.255 -  The component directories listed in the catalog file are treated as relative
   2.256 -  to the given base directory.
   2.257 -
   2.258 -  See also \secref{sec:tool-components} for some tool-support for resolving
   2.259 -  components that are formally initialized but not installed yet.
   2.260 -\<close>
   2.261 -
   2.262 -
   2.263 -section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
   2.264 -
   2.265 -text \<open>
   2.266 -  The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
   2.267 -  Isabelle related utilities, user interfaces etc. Such tools automatically
   2.268 -  benefit from the settings mechanism. All Isabelle command-line tools are
   2.269 -  invoked via a common wrapper --- @{executable_ref isabelle}:
   2.270 -  @{verbatim [display]
   2.271 -\<open>Usage: isabelle TOOL [ARGS ...]
   2.272 -
   2.273 -  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
   2.274 -
   2.275 -Available tools:
   2.276 -  ...\<close>}
   2.277 -
   2.278 -  In principle, Isabelle tools are ordinary executable scripts that are run
   2.279 -  within the Isabelle settings environment, see \secref{sec:settings}. The set
   2.280 -  of available tools is collected by @{executable isabelle} from the
   2.281 -  directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
   2.282 -  call the scripts directly from the shell. Neither should you add the tool
   2.283 -  directories to your shell's search path!
   2.284 -\<close>
   2.285 -
   2.286 -
   2.287 -subsubsection \<open>Examples\<close>
   2.288 -
   2.289 -text \<open>
   2.290 -  Show the list of available documentation of the Isabelle distribution:
   2.291 -  @{verbatim [display] \<open>isabelle doc\<close>}
   2.292 -
   2.293 -  View a certain document as follows:
   2.294 -  @{verbatim [display] \<open>isabelle doc system\<close>}
   2.295 -
   2.296 -  Query the Isabelle settings environment:
   2.297 -  @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
   2.298 -\<close>
   2.299 -
   2.300 -
   2.301 -section \<open>The raw Isabelle ML process\<close>
   2.302 -
   2.303 -subsection \<open>Batch mode \label{sec:tool-process}\<close>
   2.304 -
   2.305 -text \<open>
   2.306 -  The @{tool_def process} tool runs the raw ML process in batch mode:
   2.307 -  @{verbatim [display]
   2.308 -\<open>Usage: isabelle process [OPTIONS]
   2.309 -
   2.310 -  Options are:
   2.311 -    -d DIR       include session directory
   2.312 -    -e ML_EXPR   evaluate ML expression on startup
   2.313 -    -f ML_FILE   evaluate ML file on startup
   2.314 -    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
   2.315 -    -m MODE      add print mode for output
   2.316 -    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   2.317 -
   2.318 -  Run the raw Isabelle ML process in batch mode.\<close>}
   2.319 -\<close>
   2.320 -
   2.321 -
   2.322 -subsubsection \<open>Options\<close>
   2.323 -
   2.324 -text \<open>
   2.325 -  Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
   2.326 -  started. The source is either given literally or taken from a file. Multiple
   2.327 -  \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
   2.328 -  premature exit of the ML process with return code 1.
   2.329 -
   2.330 -  \<^medskip>
   2.331 -  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies
   2.332 -  additional directories for session roots, see also \secref{sec:tool-build}.
   2.333 -
   2.334 -  \<^medskip>
   2.335 -  The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
   2.336 -  session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
   2.337 -  mathematical Isabelle symbols.
   2.338 -
   2.339 -  \<^medskip>
   2.340 -  Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
   2.341 -  see also \secref{sec:system-options}.
   2.342 -\<close>
   2.343 -
   2.344 -
   2.345 -subsubsection \<open>Example\<close>
   2.346 -
   2.347 -text \<open>
   2.348 -  The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
   2.349 -  loader within ML:
   2.350 -  @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}
   2.351 -
   2.352 -  Observe the delicate quoting rules for the Bash shell vs.\ ML. The
   2.353 -  Isabelle/ML and Scala libraries provide functions for that, but here we need
   2.354 -  to do it manually.
   2.355 -\<close>
   2.356 -
   2.357 -
   2.358 -subsection \<open>Interactive mode\<close>
   2.359 -
   2.360 -text \<open>
   2.361 -  The @{tool_def console} tool runs the raw ML process with interactive
   2.362 -  console and line editor:
   2.363 -  @{verbatim [display]
   2.364 -\<open>Usage: isabelle console [OPTIONS]
   2.365 -
   2.366 -  Options are:
   2.367 -    -d DIR       include session directory
   2.368 -    -l NAME      logic session name (default ISABELLE_LOGIC)
   2.369 -    -m MODE      add print mode for output
   2.370 -    -n           no build of session image on startup
   2.371 -    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   2.372 -    -r           logic session is RAW_ML_SYSTEM
   2.373 -    -s           system build mode for session image
   2.374 -
   2.375 -  Build a logic session image and run the raw Isabelle ML process
   2.376 -  in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
   2.377 -
   2.378 -  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
   2.379 -  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
   2.380 -  abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
   2.381 -  Isabelle/Pure interactively.
   2.382 -
   2.383 -  Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
   2.384 -  (\secref{sec:tool-process}).
   2.385 -
   2.386 -  Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build}
   2.387 -  (\secref{sec:tool-build}).
   2.388 -
   2.389 -  \<^medskip>
   2.390 -  The Isabelle/ML process is run through the line editor that is specified via
   2.391 -  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
   2.392 -  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
   2.393 -  standard input/output.
   2.394 -
   2.395 -  The user is connected to the raw ML toplevel loop: this is neither
   2.396 -  Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
   2.397 -  relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
   2.398 -  use_thys}.
   2.399 -\<close>
   2.400 -
   2.401 -
   2.402 -section \<open>YXML versus XML\<close>
   2.403 -
   2.404 -text \<open>
   2.405 -  Isabelle tools often use YXML, which is a simple and efficient syntax for
   2.406 -  untyped XML trees. The YXML format is defined as follows.
   2.407 -
   2.408 -    \<^enum> The encoding is always UTF-8.
   2.409 -
   2.410 -    \<^enum> Body text is represented verbatim (no escaping, no special treatment of
   2.411 -    white space, no named entities, no CDATA chunks, no comments).
   2.412 -
   2.413 -    \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
   2.414 -    and \<open>\<^bold>Y = 6\<close> as follows:
   2.415 -
   2.416 -    \begin{tabular}{ll}
   2.417 -      XML & YXML \\\hline
   2.418 -      \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
   2.419 -      \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
   2.420 -      \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
   2.421 -    \end{tabular}
   2.422 -
   2.423 -    There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
   2.424 -    like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
   2.425 -    well-formed XML documents.
   2.426 -
   2.427 -  Parsing YXML is pretty straight-forward: split the text into chunks
   2.428 -  separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
   2.429 -  Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
   2.430 -  indicates close of an element. Any other non-empty chunk consists of plain
   2.431 -  text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
   2.432 -  "~~/src/Pure/PIDE/yxml.scala"}.
   2.433 -
   2.434 -  YXML documents may be detected quickly by checking that the first two
   2.435 -  characters are \<open>\<^bold>X\<^bold>Y\<close>.
   2.436 -\<close>
   2.437 -
   2.438 -end
   2.439 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Doc/System/Environment.thy	Wed Mar 16 21:14:59 2016 +0100
     3.3 @@ -0,0 +1,435 @@
     3.4 +(*:maxLineLen=78:*)
     3.5 +
     3.6 +theory Environment
     3.7 +imports Base
     3.8 +begin
     3.9 +
    3.10 +chapter \<open>The Isabelle system environment\<close>
    3.11 +
    3.12 +text \<open>
    3.13 +  This manual describes Isabelle together with related tools as seen from a
    3.14 +  system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
    3.15 +  "isabelle-isar-ref"} for the actual Isabelle input language and related
    3.16 +  concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
    3.17 +  "isabelle-implementation"} for the main concepts of the underlying
    3.18 +  implementation in Isabelle/ML.
    3.19 +\<close>
    3.20 +
    3.21 +
    3.22 +section \<open>Isabelle settings \label{sec:settings}\<close>
    3.23 +
    3.24 +text \<open>
    3.25 +  Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the
    3.26 +  process environment. This is a statically scoped collection of environment
    3.27 +  variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
    3.28 +  ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
    3.29 +  shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
    3.30 +  explained below.
    3.31 +\<close>
    3.32 +
    3.33 +
    3.34 +subsection \<open>Bootstrapping the environment \label{sec:boot}\<close>
    3.35 +
    3.36 +text \<open>
    3.37 +  Isabelle executables need to be run within a proper settings environment.
    3.38 +  This is bootstrapped as described below, on the first invocation of one of
    3.39 +  the outer wrapper scripts (such as @{executable_ref isabelle}). This happens
    3.40 +  only once for each process tree, i.e.\ the environment is passed to
    3.41 +  subprocesses according to regular Unix conventions.
    3.42 +
    3.43 +    \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined
    3.44 +    automatically from the location of the binary that has been run.
    3.45 +
    3.46 +    You should not try to set @{setting ISABELLE_HOME} manually. Also note
    3.47 +    that the Isabelle executables either have to be run from their original
    3.48 +    location in the distribution directory, or via the executable objects
    3.49 +    created by the @{tool install} tool. Symbolic links are admissible, but a
    3.50 +    plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work!
    3.51 +
    3.52 +    \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
    3.53 +    @{executable_ref bash} shell script with the auto-export option for
    3.54 +    variables enabled.
    3.55 +
    3.56 +    This file holds a rather long list of shell variable assignments, thus
    3.57 +    providing the site-wide default settings. The Isabelle distribution
    3.58 +    already contains a global settings file with sensible defaults for most
    3.59 +    variables. When installing the system, only a few of these may have to be
    3.60 +    adapted (probably @{setting ML_SYSTEM} etc.).
    3.61 +
    3.62 +    \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
    3.63 +    exists) is run in the same way as the site default settings. Note that the
    3.64 +    variable @{setting ISABELLE_HOME_USER} has already been set before ---
    3.65 +    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
    3.66 +
    3.67 +    Thus individual users may override the site-wide defaults. Typically, a
    3.68 +    user settings file contains only a few lines, with some assignments that
    3.69 +    are actually changed. Never copy the central @{file
    3.70 +    "$ISABELLE_HOME/etc/settings"} file!
    3.71 +
    3.72 +  Since settings files are regular GNU @{executable_def bash} scripts, one may
    3.73 +  use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
    3.74 +  variables depending on the system architecture or other environment
    3.75 +  variables. Such advanced features should be added only with great care,
    3.76 +  though. In particular, external environment references should be kept at a
    3.77 +  minimum.
    3.78 +
    3.79 +  \<^medskip>
    3.80 +  A few variables are somewhat special:
    3.81 +
    3.82 +    \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
    3.83 +    name of the @{executable isabelle} executables.
    3.84 +
    3.85 +    \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
    3.86 +    distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
    3.87 +    @{setting ML_IDENTIFIER}) appended automatically to its value.
    3.88 +
    3.89 +  \<^medskip>
    3.90 +  Note that the settings environment may be inspected with the @{tool getenv}
    3.91 +  tool. This might help to figure out the effect of complex settings scripts.
    3.92 +\<close>
    3.93 +
    3.94 +
    3.95 +subsection \<open>Common variables\<close>
    3.96 +
    3.97 +text \<open>
    3.98 +  This is a reference of common Isabelle settings variables. Note that the
    3.99 +  list is somewhat open-ended. Third-party utilities or interfaces may add
   3.100 +  their own selection. Variables that are special in some sense are marked
   3.101 +  with \<open>\<^sup>*\<close>.
   3.102 +
   3.103 +  \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory.
   3.104 +  On Unix systems this is usually the same as @{setting HOME}, but on Windows
   3.105 +  it is the regular home directory of the user, not the one of within the
   3.106 +  Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
   3.107 +  HOME should point to the @{file_unchecked "/home"} directory tree or the
   3.108 +  Windows user home.\<close>
   3.109 +
   3.110 +  \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
   3.111 +  Isabelle distribution directory. This is automatically determined from the
   3.112 +  Isabelle executable that has been invoked. Do not attempt to set @{setting
   3.113 +  ISABELLE_HOME} yourself from the shell!
   3.114 +
   3.115 +  \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
   3.116 +  @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked
   3.117 +  "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
   3.118 +  global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
   3.119 +  mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
   3.120 +  defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
   3.121 +
   3.122 +  \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
   3.123 +  general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
   3.124 +  platform-dependent tools usually need to refer to the more specific
   3.125 +  identification according to @{setting ISABELLE_PLATFORM}, @{setting
   3.126 +  ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
   3.127 +
   3.128 +  \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
   3.129 +  identifier for the underlying hardware and operating system. The Isabelle
   3.130 +  platform identification always refers to the 32 bit variant, even this is a
   3.131 +  64 bit machine. Note that the ML or Java runtime may have a different idea,
   3.132 +  depending on which binaries are actually run.
   3.133 +
   3.134 +  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
   3.135 +  ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
   3.136 +  that supports this; the value is empty for 32 bit. Note that the following
   3.137 +  bash expression (including the quotes) prefers the 64 bit platform, if that
   3.138 +  is available:
   3.139 +
   3.140 +  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
   3.141 +
   3.142 +  \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
   3.143 +  of the @{executable isabelle} executable. Thus other tools and scripts need
   3.144 +  not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current
   3.145 +  search path of the shell.
   3.146 +
   3.147 +  \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
   3.148 +  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
   3.149 +
   3.150 +  \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
   3.151 +  ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
   3.152 +  specify the underlying ML system to be used for Isabelle. There is only a
   3.153 +  fixed set of admissable @{setting ML_SYSTEM} names (see the @{file
   3.154 +  "$ISABELLE_HOME/etc/settings"} file of the distribution).
   3.155 +
   3.156 +  The actual compiler binary will be run from the directory @{setting
   3.157 +  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
   3.158 +  The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
   3.159 +  images, which is useful for cross-platform installations. The value of
   3.160 +  @{setting ML_IDENTIFIER} is automatically obtained by composing the values
   3.161 +  of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
   3.162 +  values.
   3.163 +
   3.164 +  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
   3.165 +  Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
   3.166 +  essential for Isabelle/Scala and other JVM-based tools to work properly.
   3.167 +  Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
   3.168 +  Environment), not JDK.
   3.169 +
   3.170 +  \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
   3.171 +  colons) where Isabelle logic images may reside. When looking up heaps files,
   3.172 +  the value of @{setting ML_IDENTIFIER} is appended to each component
   3.173 +  internally.
   3.174 +
   3.175 +  \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
   3.176 +  should be stored by default. The ML system and Isabelle version identifier
   3.177 +  is appended here, too.
   3.178 +
   3.179 +  \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
   3.180 +  browser information is stored as HTML and PDF (see also \secref{sec:info}).
   3.181 +  The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
   3.182 +
   3.183 +  \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
   3.184 +  is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
   3.185 +
   3.186 +  \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
   3.187 +  @{tool_ref console} interface.
   3.188 +
   3.189 +  \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
   3.190 +  @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
   3.191 +  document preparation (see also \secref{sec:tool-latex}).
   3.192 +
   3.193 +  \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
   3.194 +  that are scanned by @{executable isabelle} for external utility programs
   3.195 +  (see also \secref{sec:isabelle-tool}).
   3.196 +
   3.197 +  \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories
   3.198 +  with documentation files.
   3.199 +
   3.200 +  \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
   3.201 +  \<^verbatim>\<open>pdf\<close> files.
   3.202 +
   3.203 +  \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying
   3.204 +  \<^verbatim>\<open>dvi\<close> files.
   3.205 +
   3.206 +  \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
   3.207 +  running Isabelle ML process derives an individual directory for temporary
   3.208 +  files.
   3.209 +\<close>
   3.210 +
   3.211 +
   3.212 +subsection \<open>Additional components \label{sec:components}\<close>
   3.213 +
   3.214 +text \<open>
   3.215 +  Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The
   3.216 +  general layout conventions are that of the main Isabelle distribution
   3.217 +  itself, and the following two files (both optional) have a special meaning:
   3.218 +
   3.219 +    \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
   3.220 +    bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
   3.221 +    usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the
   3.222 +    component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
   3.223 +
   3.224 +    For example, the following setting allows to refer to files within the
   3.225 +    component later on, without having to hardwire absolute paths:
   3.226 +    @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
   3.227 +
   3.228 +    Components can also add to existing Isabelle settings such as
   3.229 +    @{setting_def ISABELLE_TOOLS}, in order to provide component-specific
   3.230 +    tools that can be invoked by end-users. For example:
   3.231 +    @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
   3.232 +
   3.233 +    \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same
   3.234 +    structure. The directory specifications given here can be either absolute
   3.235 +    (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory.
   3.236 +
   3.237 +  The root of component initialization is @{setting ISABELLE_HOME} itself.
   3.238 +  After initializing all of its sub-components recursively, @{setting
   3.239 +  ISABELLE_HOME_USER} is included in the same manner (if that directory
   3.240 +  exists). This allows to install private components via @{file_unchecked
   3.241 +  "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
   3.242 +  to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
   3.243 +  \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
   3.244 +  directory). For example:
   3.245 +  @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
   3.246 +
   3.247 +  This is tolerant wrt.\ missing component directories, but might produce a
   3.248 +  warning.
   3.249 +
   3.250 +  \<^medskip>
   3.251 +  More complex situations may be addressed by initializing components listed
   3.252 +  in a given catalog file, relatively to some base directory:
   3.253 +  @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}
   3.254 +
   3.255 +  The component directories listed in the catalog file are treated as relative
   3.256 +  to the given base directory.
   3.257 +
   3.258 +  See also \secref{sec:tool-components} for some tool-support for resolving
   3.259 +  components that are formally initialized but not installed yet.
   3.260 +\<close>
   3.261 +
   3.262 +
   3.263 +section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
   3.264 +
   3.265 +text \<open>
   3.266 +  The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
   3.267 +  Isabelle related utilities, user interfaces etc. Such tools automatically
   3.268 +  benefit from the settings mechanism. All Isabelle command-line tools are
   3.269 +  invoked via a common wrapper --- @{executable_ref isabelle}:
   3.270 +  @{verbatim [display]
   3.271 +\<open>Usage: isabelle TOOL [ARGS ...]
   3.272 +
   3.273 +  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
   3.274 +
   3.275 +Available tools:
   3.276 +  ...\<close>}
   3.277 +
   3.278 +  In principle, Isabelle tools are ordinary executable scripts that are run
   3.279 +  within the Isabelle settings environment, see \secref{sec:settings}. The set
   3.280 +  of available tools is collected by @{executable isabelle} from the
   3.281 +  directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
   3.282 +  call the scripts directly from the shell. Neither should you add the tool
   3.283 +  directories to your shell's search path!
   3.284 +\<close>
   3.285 +
   3.286 +
   3.287 +subsubsection \<open>Examples\<close>
   3.288 +
   3.289 +text \<open>
   3.290 +  Show the list of available documentation of the Isabelle distribution:
   3.291 +  @{verbatim [display] \<open>isabelle doc\<close>}
   3.292 +
   3.293 +  View a certain document as follows:
   3.294 +  @{verbatim [display] \<open>isabelle doc system\<close>}
   3.295 +
   3.296 +  Query the Isabelle settings environment:
   3.297 +  @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
   3.298 +\<close>
   3.299 +
   3.300 +
   3.301 +section \<open>The raw Isabelle ML process\<close>
   3.302 +
   3.303 +subsection \<open>Batch mode \label{sec:tool-process}\<close>
   3.304 +
   3.305 +text \<open>
   3.306 +  The @{tool_def process} tool runs the raw ML process in batch mode:
   3.307 +  @{verbatim [display]
   3.308 +\<open>Usage: isabelle process [OPTIONS]
   3.309 +
   3.310 +  Options are:
   3.311 +    -d DIR       include session directory
   3.312 +    -e ML_EXPR   evaluate ML expression on startup
   3.313 +    -f ML_FILE   evaluate ML file on startup
   3.314 +    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
   3.315 +    -m MODE      add print mode for output
   3.316 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   3.317 +
   3.318 +  Run the raw Isabelle ML process in batch mode.\<close>}
   3.319 +\<close>
   3.320 +
   3.321 +
   3.322 +subsubsection \<open>Options\<close>
   3.323 +
   3.324 +text \<open>
   3.325 +  Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
   3.326 +  started. The source is either given literally or taken from a file. Multiple
   3.327 +  \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
   3.328 +  premature exit of the ML process with return code 1.
   3.329 +
   3.330 +  \<^medskip>
   3.331 +  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies
   3.332 +  additional directories for session roots, see also \secref{sec:tool-build}.
   3.333 +
   3.334 +  \<^medskip>
   3.335 +  The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
   3.336 +  session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
   3.337 +  mathematical Isabelle symbols.
   3.338 +
   3.339 +  \<^medskip>
   3.340 +  Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
   3.341 +  see also \secref{sec:system-options}.
   3.342 +\<close>
   3.343 +
   3.344 +
   3.345 +subsubsection \<open>Example\<close>
   3.346 +
   3.347 +text \<open>
   3.348 +  The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
   3.349 +  loader within ML:
   3.350 +  @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}
   3.351 +
   3.352 +  Observe the delicate quoting rules for the Bash shell vs.\ ML. The
   3.353 +  Isabelle/ML and Scala libraries provide functions for that, but here we need
   3.354 +  to do it manually.
   3.355 +\<close>
   3.356 +
   3.357 +
   3.358 +subsection \<open>Interactive mode\<close>
   3.359 +
   3.360 +text \<open>
   3.361 +  The @{tool_def console} tool runs the raw ML process with interactive
   3.362 +  console and line editor:
   3.363 +  @{verbatim [display]
   3.364 +\<open>Usage: isabelle console [OPTIONS]
   3.365 +
   3.366 +  Options are:
   3.367 +    -d DIR       include session directory
   3.368 +    -l NAME      logic session name (default ISABELLE_LOGIC)
   3.369 +    -m MODE      add print mode for output
   3.370 +    -n           no build of session image on startup
   3.371 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   3.372 +    -r           logic session is RAW_ML_SYSTEM
   3.373 +    -s           system build mode for session image
   3.374 +
   3.375 +  Build a logic session image and run the raw Isabelle ML process
   3.376 +  in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
   3.377 +
   3.378 +  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
   3.379 +  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
   3.380 +  abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
   3.381 +  Isabelle/Pure interactively.
   3.382 +
   3.383 +  Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
   3.384 +  (\secref{sec:tool-process}).
   3.385 +
   3.386 +  Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build}
   3.387 +  (\secref{sec:tool-build}).
   3.388 +
   3.389 +  \<^medskip>
   3.390 +  The Isabelle/ML process is run through the line editor that is specified via
   3.391 +  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
   3.392 +  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
   3.393 +  standard input/output.
   3.394 +
   3.395 +  The user is connected to the raw ML toplevel loop: this is neither
   3.396 +  Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
   3.397 +  relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
   3.398 +  use_thys}.
   3.399 +\<close>
   3.400 +
   3.401 +
   3.402 +section \<open>YXML versus XML\<close>
   3.403 +
   3.404 +text \<open>
   3.405 +  Isabelle tools often use YXML, which is a simple and efficient syntax for
   3.406 +  untyped XML trees. The YXML format is defined as follows.
   3.407 +
   3.408 +    \<^enum> The encoding is always UTF-8.
   3.409 +
   3.410 +    \<^enum> Body text is represented verbatim (no escaping, no special treatment of
   3.411 +    white space, no named entities, no CDATA chunks, no comments).
   3.412 +
   3.413 +    \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
   3.414 +    and \<open>\<^bold>Y = 6\<close> as follows:
   3.415 +
   3.416 +    \begin{tabular}{ll}
   3.417 +      XML & YXML \\\hline
   3.418 +      \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
   3.419 +      \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
   3.420 +      \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
   3.421 +    \end{tabular}
   3.422 +
   3.423 +    There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
   3.424 +    like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
   3.425 +    well-formed XML documents.
   3.426 +
   3.427 +  Parsing YXML is pretty straight-forward: split the text into chunks
   3.428 +  separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
   3.429 +  Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
   3.430 +  indicates close of an element. Any other non-empty chunk consists of plain
   3.431 +  text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
   3.432 +  "~~/src/Pure/PIDE/yxml.scala"}.
   3.433 +
   3.434 +  YXML documents may be detected quickly by checking that the first two
   3.435 +  characters are \<open>\<^bold>X\<^bold>Y\<close>.
   3.436 +\<close>
   3.437 +
   3.438 +end
   3.439 \ No newline at end of file
     4.1 --- a/src/Doc/System/document/root.tex	Wed Mar 16 21:11:15 2016 +0100
     4.2 +++ b/src/Doc/System/document/root.tex	Wed Mar 16 21:14:59 2016 +0100
     4.3 @@ -30,7 +30,7 @@
     4.4  \maketitle 
     4.5  \pagenumbering{roman} \tableofcontents \clearfirst
     4.6  
     4.7 -\input{Basics.tex}
     4.8 +\input{Environment.tex}
     4.9  \input{Sessions.tex}
    4.10  \input{Presentation.tex}
    4.11  \input{Scala.tex}