src/Doc/System/Misc.thy
author wenzelm
Tue, 20 Nov 2012 15:18:11 +0100
changeset 50132 180d086c30dd
parent 49072 747835eb2782
child 50653 5c85f8b80b95
permissions -rw-r--r--
simplified command line of "isabelle install";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     1
theory Misc
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 41512
diff changeset
     2
imports Base
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     3
begin
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     4
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     5
chapter {* Miscellaneous tools \label{ch:tools} *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     6
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     7
text {*
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     8
  Subsequently we describe various Isabelle related utilities, given
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     9
  in alphabetical order.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    10
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    11
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    12
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    13
section {* Resolving Isabelle components \label{sec:tool-components} *}
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    14
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    15
text {*
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    16
  The @{tool_def components} tool resolves Isabelle components:
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    17
\begin{ttbox}
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    18
Usage: isabelle components [OPTIONS] [COMPONENTS ...]
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    19
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    20
  Options are:
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    21
    -R URL       component repository
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    22
                 (default $ISABELLE_COMPONENT_REPOSITORY)
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    23
    -a           all missing components
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    24
    -l           list status
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    25
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    26
  Resolve Isabelle components via download and installation.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    27
  COMPONENTS are identified via base name.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    28
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    29
  ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    30
\end{ttbox}
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    31
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    32
  Components are initialized as described in \secref{sec:components}
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    33
  in a permissive manner, which can mark components as ``missing''.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    34
  This state is amended by letting @{tool "components"} download and
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    35
  unpack components that are published on the default component
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    36
  repository \url{http://isabelle.in.tum.de/components/} in
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    37
  particular.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    38
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    39
  Option @{verbatim "-R"} specifies an alternative component
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    40
  repository.  Note that @{verbatim "file:///"} URLs can be used for
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    41
  local directories.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    42
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    43
  Option @{verbatim "-a"} selects all missing components to be
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    44
  installed.  Explicit components may be named as command
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    45
  line-arguments as well.  Note that components are uniquely
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    46
  identified by their base name, while the installation takes place in
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    47
  the location that was specified in the attempt to initialize the
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    48
  component before.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    49
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    50
  Option @{verbatim "-l"} lists the current state of available and
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    51
  missing components with their location (full name) within the
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    52
  file-system.  *}
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    53
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    54
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    55
section {* Displaying documents *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    56
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    57
text {* The @{tool_def display} tool displays documents in DVI or PDF
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    58
  format:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    59
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    60
Usage: isabelle display [OPTIONS] FILE
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    61
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    62
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    63
    -c           cleanup -- remove FILE after use
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    64
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    65
  Display document FILE (in DVI format).
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    66
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    67
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    68
  \medskip The @{verbatim "-c"} option causes the input file to be
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    69
  removed after use.  The program for viewing @{verbatim dvi} files is
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    70
  determined by the @{setting DVI_VIEWER} setting.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    71
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    72
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    73
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    74
section {* Viewing documentation \label{sec:tool-doc} *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    75
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    76
text {*
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    77
  The @{tool_def doc} tool displays online documentation:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    78
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    79
Usage: isabelle doc [DOC]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    80
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    81
  View Isabelle documentation DOC, or show list of available documents.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    82
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    83
  If called without arguments, it lists all available documents. Each
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    84
  line starts with an identifier, followed by a short description. Any
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    85
  of these identifiers may be specified as the first argument in order
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    86
  to have the corresponding document displayed.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    87
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    88
  \medskip The @{setting ISABELLE_DOCS} setting specifies the list of
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    89
  directories (separated by colons) to be scanned for documentations.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    90
  The program for viewing @{verbatim dvi} files is determined by the
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    91
  @{setting DVI_VIEWER} setting.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    92
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    93
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    94
47828
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    95
section {* Shell commands within the settings environment \label{sec:tool-env} *}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    96
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    97
text {* The @{tool_def env} tool is a direct wrapper for the standard
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    98
  @{verbatim "/usr/bin/env"} command on POSIX systems, running within
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    99
  the Isabelle settings environment (\secref{sec:settings}).
47828
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   100
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   101
  The command-line arguments are that of the underlying version of
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   102
  @{verbatim env}.  For example, the following invokes an instance of
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   103
  the GNU Bash shell within the Isabelle environment:
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   104
\begin{alltt}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   105
  isabelle env bash
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   106
\end{alltt}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   107
*}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   108
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   109
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   110
section {* Getting logic images *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   111
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   112
text {* The @{tool_def findlogics} tool traverses all directories
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   113
  specified in @{setting ISABELLE_PATH}, looking for Isabelle logic
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   114
  images. Its usage is:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   115
\begin{ttbox}
48577
wenzelm
parents: 47828
diff changeset
   116
Usage: isabelle findlogics
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   117
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   118
  Collect heap file names from ISABELLE_PATH.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   119
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   120
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   121
  The base names of all files found on the path are printed --- sorted
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   122
  and with duplicates removed. Also note that lookup in @{setting
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   123
  ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   124
  and @{setting ML_PLATFORM}. Thus switching to another ML compiler
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   125
  may change the set of logic images available.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   126
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   127
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   128
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   129
section {* Inspecting the settings environment \label{sec:tool-getenv} *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   130
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   131
text {* The Isabelle settings environment --- as provided by the
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   132
  site-default and user-specific settings files --- can be inspected
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   133
  with the @{tool_def getenv} tool:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   134
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   135
Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   136
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   137
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   138
    -a           display complete environment
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   139
    -b           print values only (doesn't work for -a)
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   140
    -d FILE      dump complete environment to FILE
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   141
                 (null terminated entries)
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   142
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   143
  Get value of VARNAMES from the Isabelle settings.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   144
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   145
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   146
  With the @{verbatim "-a"} option, one may inspect the full process
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   147
  environment that Isabelle related programs are run in. This usually
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   148
  contains much more variables than are actually Isabelle settings.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   149
  Normally, output is a list of lines of the form @{text
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   150
  name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   151
  causes only the values to be printed.
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   152
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   153
  Option @{verbatim "-d"} produces a dump of the complete environment
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   154
  to the specified file.  Entries are terminated by the ASCII null
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   155
  character, i.e.\ the C string terminator.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   156
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   157
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   158
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   159
subsubsection {* Examples *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   160
48815
wenzelm
parents: 48814
diff changeset
   161
text {* Get the location of @{setting ISABELLE_HOME_USER} where
wenzelm
parents: 48814
diff changeset
   162
  user-specific information is stored:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   163
\begin{ttbox}
48815
wenzelm
parents: 48814
diff changeset
   164
isabelle getenv ISABELLE_HOME_USER
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   165
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   166
48815
wenzelm
parents: 48814
diff changeset
   167
  \medskip Get the value only of the same settings variable, which is
wenzelm
parents: 48814
diff changeset
   168
particularly useful in shell scripts:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   169
\begin{ttbox}
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28253
diff changeset
   170
isabelle getenv -b ISABELLE_OUTPUT
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   171
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   172
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   173
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   174
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   175
section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   176
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   177
text {* By default, the main Isabelle binaries (@{executable
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   178
  "isabelle"} etc.)  are just run from their location within the
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   179
  distribution directory, probably indirectly by the shell through its
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   180
  @{setting PATH}.  Other schemes of installation are supported by the
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   181
  @{tool_def install} tool:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   182
\begin{ttbox}
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   183
Usage: isabelle install [OPTIONS] BINDIR
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   184
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   185
  Options are:
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   186
    -d DISTDIR   refer to DISTDIR as Isabelle distribution
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   187
                 (default ISABELLE_HOME)
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   188
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   189
  Install Isabelle executables with absolute references to the
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   190
  distribution directory.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   191
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   192
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   193
  The @{verbatim "-d"} option overrides the current Isabelle
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   194
  distribution directory as determined by @{setting ISABELLE_HOME}.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   195
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   196
  The @{text BINDIR} argument tells where executable wrapper scripts
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   197
  for @{executable "isabelle-process"} and @{executable isabelle}
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   198
  should be placed, which is typically a directory in the shell's
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   199
  @{setting PATH}, such as @{verbatim "$HOME/bin"}.
48815
wenzelm
parents: 48814
diff changeset
   200
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   201
  \medskip It is also possible to make symbolic links of the main
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   202
  Isabelle executables manually, but making separate copies outside
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   203
  the Isabelle distribution directory will not work!  *}
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   204
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   205
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   206
section {* Creating instances of the Isabelle logo *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   207
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   208
text {* The @{tool_def logo} tool creates instances of the generic
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   209
  Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   210
\begin{ttbox}
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   211
Usage: isabelle logo [OPTIONS] XYZ
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   212
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   213
  Create instance XYZ of the Isabelle logo (as EPS and PDF).
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   214
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   215
  Options are:
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   216
    -n NAME      alternative output base name (default "isabelle_xyx")
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   217
    -q           quiet mode
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   218
\end{ttbox}
48936
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   219
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   220
  Option @{verbatim "-n"} specifies an altenative (base) name for the
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   221
  generated files.  The default is @{verbatim "isabelle_"}@{text xyz}
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   222
  in lower-case.
48936
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   223
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   224
  Option @{verbatim "-q"} omits printing of the result file name.
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   225
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   226
  \medskip Implementors of Isabelle tools and applications are
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   227
  encouraged to make derived Isabelle logos for their own projects
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   228
  using this template.  *}
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   229
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   230
48814
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   231
section {* Isabelle wrapper for make \label{sec:tool-make} *}
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   232
48814
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   233
text {* The old @{tool_def make} tool is a very simple wrapper for
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   234
  ordinary Unix @{executable make}:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   235
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   236
Usage: isabelle make [ARGS ...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   237
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   238
  Compile the logic in current directory using IsaMakefile.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   239
  ARGS are directly passed to the system make program.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   240
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   241
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   242
  Note that the Isabelle settings environment is also active. Thus one
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   243
  may refer to its values within the @{verbatim IsaMakefile}, e.g.\
48814
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   244
  @{verbatim "$(ISABELLE_HOME)"}. Furthermore, programs started from
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   245
  the make file also inherit this environment.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   246
*}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   247
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   248
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   249
section {* Creating Isabelle session directories
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   250
  \label{sec:tool-mkdir} *}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   251
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   252
text {* The old @{tool_def mkdir} tool prepares Isabelle session
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   253
  source directories, including a sensible default setup of @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   254
  IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   255
  directory with a minimal @{verbatim root.tex} that is sufficient to
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   256
  print all theories of the session (in the order of appearance); see
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   257
  \secref{sec:tool-document} for further information on Isabelle
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   258
  document preparation.  The usage of @{tool mkdir} is:
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   259
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   260
\begin{ttbox}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   261
Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   262
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   263
  Options are:
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   264
    -I FILE      alternative IsaMakefile output
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   265
    -P           include parent logic target
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   266
    -b           setup build mode (session outputs heap image)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   267
    -q           quiet mode
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   268
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   269
  Prepare session directory, including IsaMakefile and document source,
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   270
  with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   271
\end{ttbox}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   272
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   273
  The @{tool mkdir} tool is conservative in the sense that any
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   274
  existing @{verbatim IsaMakefile} etc.\ is left unchanged.  Thus it
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   275
  is safe to invoke it multiple times, although later runs may not
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   276
  have the desired effect.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   277
48814
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   278
  Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   279
  incrementally --- manual changes are required for multiple
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   280
  sub-sessions.  On order to get an initial working session, the only
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   281
  editing needed is to add appropriate @{ML use_thy} calls to the
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   282
  generated @{verbatim ROOT.ML} file.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   283
*}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   284
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   285
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   286
subsubsection {* Options *}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   287
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   288
text {*
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   289
  The @{verbatim "-I"} option specifies an alternative to @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   290
  IsaMakefile} for dependencies.  Note that ``@{verbatim "-"}'' refers
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   291
  to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   292
  to peek at @{tool mkdir}'s idea of @{tool make} setup required for
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   293
  some particular of Isabelle session.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   294
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   295
  \medskip The @{verbatim "-P"} option includes a target for the
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   296
  parent @{verbatim LOGIC} session in the generated @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   297
  IsaMakefile}.  The corresponding sources are assumed to be located
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   298
  within the Isabelle distribution.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   299
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   300
  \medskip The @{verbatim "-b"} option sets up the current directory
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   301
  as the base for a new session that provides an actual logic image,
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   302
  as opposed to one that only runs several theories based on an
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   303
  existing image.  Note that in the latter case, everything except
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   304
  @{verbatim IsaMakefile} would be placed into a separate directory
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   305
  @{verbatim NAME}, rather than the current one.  See
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   306
  \secref{sec:tool-usedir} for further information on \emph{build
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   307
  mode} vs.\ \emph{example mode} of @{tool usedir}.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   308
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   309
  \medskip The @{verbatim "-q"} option enables quiet mode, suppressing
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   310
  further notes on how to proceed.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   311
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   312
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   313
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   314
section {* Printing documents *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   315
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   316
text {*
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   317
  The @{tool_def print} tool prints documents:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   318
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   319
Usage: isabelle print [OPTIONS] FILE
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   320
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   321
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   322
    -c           cleanup -- remove FILE after use
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   323
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   324
  Print document FILE.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   325
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   326
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   327
  The @{verbatim "-c"} option causes the input file to be removed
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   328
  after use.  The printer spool command is determined by the @{setting
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   329
  PRINT_COMMAND} setting.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   330
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   331
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   332
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   333
section {* Remove awkward symbol names from theory sources *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   334
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   335
text {*
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   336
  The @{tool_def unsymbolize} tool tunes Isabelle theory sources to
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   337
  improve readability for plain ASCII output (e.g.\ in email
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   338
  communication).  Most notably, @{tool unsymbolize} replaces awkward
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   339
  arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   340
  by @{verbatim "==>"}.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   341
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   342
Usage: isabelle unsymbolize [FILES|DIRS...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   343
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   344
  Recursively find .thy/.ML files, removing unreadable symbol names.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   345
  Note: this is an ad-hoc script; there is no systematic way to replace
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   346
  symbols independently of the inner syntax of a theory!
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   347
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   348
  Renames old versions of FILES by appending "~~".
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   349
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   350
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   351
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   352
48814
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   353
section {* Running Isabelle sessions \label{sec:tool-usedir} *}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   354
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   355
text {* The old @{tool_def usedir} tool builds object-logic images, or
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   356
  runs example sessions based on existing logics. Its usage is:
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   357
\begin{ttbox}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   358
Usage: isabelle usedir [OPTIONS] LOGIC NAME
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   359
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   360
  Options are:
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   361
    -C BOOL      copy existing document directory to -D PATH (default true)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   362
    -D PATH      dump generated document sources into PATH
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   363
    -M MAX       multithreading: maximum number of worker threads (default 1)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   364
    -P PATH      set path for remote theory browsing information
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   365
    -Q INT       set threshold for sub-proof parallelization (default 50)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   366
    -T LEVEL     multithreading: trace level (default 0)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   367
    -V VARIANT   declare alternative document VARIANT
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   368
    -b           build mode (output heap image, using current dir)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   369
    -d FORMAT    build document as FORMAT (default false)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   370
    -f NAME      use ML file NAME (default ROOT.ML)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   371
    -g BOOL      generate session graph image for document (default false)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   372
    -i BOOL      generate theory browser information (default false)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   373
    -m MODE      add print mode for output
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   374
    -p LEVEL     set level of detail for proof objects (default 0)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   375
    -q LEVEL     set level of parallel proof checking (default 1)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   376
    -r           reset session path
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   377
    -s NAME      override session NAME
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   378
    -t BOOL      internal session timing (default false)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   379
    -v BOOL      be verbose (default false)
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   380
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   381
  Build object-logic or run examples. Also creates browsing
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   382
  information (HTML etc.) according to settings.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   383
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   384
  ISABELLE_USEDIR_OPTIONS=...
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   385
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   386
  ML_PLATFORM=...
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   387
  ML_HOME=...
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   388
  ML_SYSTEM=...
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   389
  ML_OPTIONS=...
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   390
\end{ttbox}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   391
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   392
  Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   393
  setting is implicitly prefixed to \emph{any} @{tool usedir}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   394
  call. Since the @{verbatim IsaMakefile}s of all object-logics
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   395
  distributed with Isabelle just invoke @{tool usedir} for the real
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   396
  work, one may control compilation options globally via above
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   397
  variable. In particular, generation of \rmindex{HTML} browsing
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   398
  information and document preparation is controlled here.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   399
*}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   400
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   401
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   402
subsubsection {* Options *}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   403
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   404
text {*
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   405
  Basically, there are two different modes of operation: \emph{build
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   406
  mode} (enabled through the @{verbatim "-b"} option) and
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   407
  \emph{example mode} (default).
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   408
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   409
  Calling @{tool usedir} with @{verbatim "-b"} runs @{executable
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   410
  "isabelle-process"} with input image @{verbatim LOGIC} and output to
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   411
  @{verbatim NAME}, as provided on the command line. This will be a
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   412
  batch session, running @{verbatim ROOT.ML} from the current
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   413
  directory and then quitting.  It is assumed that @{verbatim ROOT.ML}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   414
  contains all ML commands required to build the logic.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   415
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   416
  In example mode, @{tool usedir} runs a read-only session of
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   417
  @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   418
  within directory @{verbatim NAME}.  It assumes that this file
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   419
  contains appropriate ML commands to run the desired examples.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   420
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   421
  \medskip The @{verbatim "-i"} option controls theory browser data
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   422
  generation. It may be explicitly turned on or off --- as usual, the
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   423
  last occurrence of @{verbatim "-i"} on the command line wins.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   424
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   425
  The @{verbatim "-P"} option specifies a path (or actual URL) to be
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   426
  prefixed to any \emph{non-local} reference of existing theories.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   427
  Thus user sessions may easily link to existing Isabelle libraries
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   428
  already present on the WWW.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   429
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   430
  The @{verbatim "-m"} options specifies additional print modes to be
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   431
  activated temporarily while the session is processed.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   432
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   433
  \medskip The @{verbatim "-d"} option controls document preparation.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   434
  Valid arguments are @{verbatim false} (do not prepare any document;
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   435
  this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz},
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   436
  @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}.  The logic
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   437
  session has to provide a properly setup @{verbatim document}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   438
  directory.  See \secref{sec:tool-document} and
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   439
  \secref{sec:tool-latex} for more details.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   440
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   441
  \medskip The @{verbatim "-V"} option declares alternative document
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   442
  variants, consisting of name/tags pairs (cf.\ options @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   443
  "-n"} and @{verbatim "-t"} of @{tool_ref document}).  The standard
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   444
  document is equivalent to ``@{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   445
  "document=theory,proof,ML"}'', which means that all theory begin/end
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   446
  commands, proof body texts, and ML code will be presented
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   447
  faithfully.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   448
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   449
  An alternative variant ``@{verbatim "outline=/proof/ML"}'' would
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   450
  fold proof and ML parts, replacing the original text by a short
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   451
  place-holder.  The form ``@{text name}@{verbatim "=-"},'' means to
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   452
  remove document @{text name} from the list of variants to be
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   453
  processed.  Any number of @{verbatim "-V"} options may be given;
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   454
  later declarations have precedence over earlier ones.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   455
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   456
  Some document variant @{text name} may use an alternative {\LaTeX}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   457
  entry point called @{verbatim "document/root_"}@{text
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   458
  "name"}@{verbatim ".tex"} if that file exists; otherwise the common
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   459
  @{verbatim "document/root.tex"} is used.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   460
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   461
  \medskip The @{verbatim "-g"} option produces images of the theory
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   462
  dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   463
  generated document, both as @{verbatim session_graph.eps} and
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   464
  @{verbatim session_graph.pdf} at the same time.  To include this in
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   465
  the final {\LaTeX} document one could say @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   466
  "\\includegraphics{session_graph}"} in @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   467
  "document/root.tex"} (omitting the file-name extension enables
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   468
  {\LaTeX} to select to correct version, either for the DVI or PDF
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   469
  output path).
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   470
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   471
  \medskip The @{verbatim "-D"} option causes the generated document
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   472
  sources to be dumped at location @{verbatim PATH}; this path is
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   473
  relative to the session's main directory.  If the @{verbatim "-C"}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   474
  option is true, this will include a copy of an existing @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   475
  document} directory as provided by the user.  For example, @{tool
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   476
  usedir}~@{verbatim "-D generated HOL Foo"} produces a complete set
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   477
  of document sources at @{verbatim "Foo/generated"}.  Subsequent
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   478
  invocation of @{tool document}~@{verbatim "Foo/generated"} (see also
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   479
  \secref{sec:tool-document}) will process the final result
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   480
  independently of an Isabelle job.  This decoupled mode of operation
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   481
  facilitates debugging of serious {\LaTeX} errors, for example.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   482
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   483
  \medskip The @{verbatim "-p"} option determines the level of detail
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   484
  for internal proof objects, see also the \emph{Isabelle Reference
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   485
  Manual}~\cite{isabelle-ref}.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   486
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   487
  \medskip The @{verbatim "-q"} option specifies the level of parallel
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   488
  proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   489
  proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   490
  The option @{verbatim "-Q"} specifies a threshold for @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   491
  "-q2"}: nested proofs are only parallelized when the current number
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   492
  of forked proofs falls below the given value (default 50),
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   493
  multiplied by the number of worker threads (see option @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   494
  "-M"}).
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   495
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   496
  \medskip The @{verbatim "-t"} option produces a more detailed
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   497
  internal timing report of the session.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   498
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   499
  \medskip The @{verbatim "-v"} option causes additional information
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   500
  to be printed while running the session, notably the location of
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   501
  prepared documents.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   502
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   503
  \medskip The @{verbatim "-M"} option specifies the maximum number of
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   504
  parallel worker threads used for processing independent tasks when
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   505
  checking theory sources (multithreading only works on suitable ML
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   506
  platforms).  The special value of @{verbatim 0} or @{verbatim max}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   507
  refers to the number of actual CPU cores of the underlying machine,
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   508
  which is a good starting point for optimal performance tuning.  The
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   509
  @{verbatim "-T"} option determines the level of detail in tracing
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   510
  output concerning the internal locking and scheduling in
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   511
  multithreaded operation.  This may be helpful in isolating
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   512
  performance bottle-necks, e.g.\ due to excessive wait states when
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   513
  locking critical code sections.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   514
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   515
  \medskip Any @{tool usedir} session is named by some \emph{session
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   516
  identifier}. These accumulate, documenting the way sessions depend
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   517
  on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   518
  refers to the examples of FOL, which in turn is built upon Pure.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   519
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   520
  The current session's identifier is by default just the base name of
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   521
  the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   522
  NAME} argument (in example mode). This may be overridden explicitly
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   523
  via the @{verbatim "-s"} option.
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   524
*}
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   525
d488a5f25bf6 some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
wenzelm
parents: 48736
diff changeset
   526
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   527
section {* Output the version identifier of the Isabelle distribution *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   528
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   529
text {*
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   530
  The @{tool_def version} tool displays Isabelle version information:
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   531
\begin{ttbox}
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   532
Usage: isabelle version [OPTIONS]
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   533
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   534
  Options are:
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   535
    -i           short identification (derived from Mercurial id)
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   536
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   537
  Display Isabelle version information.
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   538
\end{ttbox}
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   539
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   540
  \medskip The default is to output the full version string of the
47827
13530d774a21 updated system manual for release;
wenzelm
parents: 44799
diff changeset
   541
  Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2012: May 2012"}.
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   542
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   543
  The @{verbatim "-i"} option produces a short identification derived
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   544
  from the Mercurial id of the @{setting ISABELLE_HOME} directory.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   545
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   546
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   547
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   548
section {* Convert XML to YXML *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   549
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   550
text {*
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   551
  The @{tool_def yxml} tool converts a standard XML document (stdin)
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   552
  to the much simpler and more efficient YXML format of Isabelle
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   553
  (stdout).  The YXML format is defined as follows.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   554
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   555
  \begin{enumerate}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   556
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   557
  \item The encoding is always UTF-8.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   558
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   559
  \item Body text is represented verbatim (no escaping, no special
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   560
  treatment of white space, no named entities, no CDATA chunks, no
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   561
  comments).
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   562
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   563
  \item Markup elements are represented via ASCII control characters
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   564
  @{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   565
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   566
  \begin{tabular}{ll}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   567
    XML & YXML \\\hline
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   568
    @{verbatim "<"}@{text "name attribute"}@{verbatim "="}@{text "value \<dots>"}@{verbatim ">"} &
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   569
    @{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\<dots>\<^bold>X"} \\
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   570
    @{verbatim "</"}@{text name}@{verbatim ">"} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   571
  \end{tabular}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   572
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   573
  There is no special case for empty body text, i.e.\ @{verbatim
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   574
  "<foo/>"} is treated like @{verbatim "<foo></foo>"}.  Also note that
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   575
  @{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   576
  well-formed XML documents.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   577
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   578
  \end{enumerate}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   579
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   580
  Parsing YXML is pretty straight-forward: split the text into chunks
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   581
  separated by @{text "\<^bold>X"}, then split each chunk into
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   582
  sub-chunks separated by @{text "\<^bold>Y"}.  Markup chunks start
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   583
  with an empty sub-chunk, and a second empty sub-chunk indicates
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   584
  close of an element.  Any other non-empty chunk consists of plain
44799
1fd0a1276a09 updated file locations;
wenzelm
parents: 43564
diff changeset
   585
  text.  For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
1fd0a1276a09 updated file locations;
wenzelm
parents: 43564
diff changeset
   586
  @{file "~~/src/Pure/PIDE/yxml.scala"}.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   587
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   588
  YXML documents may be detected quickly by checking that the first
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   589
  two characters are @{text "\<^bold>X\<^bold>Y"}.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   590
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   591
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   592
end