doc-src/System/Thy/document/Misc.tex
author wenzelm
Wed, 08 Aug 2012 14:45:40 +0200
changeset 48736 292b97e17fb7
parent 48722 a5e3ba7cbb2a
child 48814 d488a5f25bf6
permissions -rw-r--r--
discontinued obsolete "isabelle makeall";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     1
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{Misc}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     4
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     5
\isadelimtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     6
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     7
\endisadelimtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     8
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     9
\isatagtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    10
\isacommand{theory}\isamarkupfalse%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    11
\ Misc\isanewline
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 41512
diff changeset
    12
\isakeyword{imports}\ Base\isanewline
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    13
\isakeyword{begin}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    14
\endisatagtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    15
{\isafoldtheory}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    16
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    17
\isadelimtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    18
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    19
\endisadelimtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    20
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    21
\isamarkupchapter{Miscellaneous tools \label{ch:tools}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    22
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    23
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    24
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    25
\begin{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    26
Subsequently we describe various Isabelle related utilities, given
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    27
  in alphabetical order.%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    28
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    29
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    30
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    31
\isamarkupsection{Displaying documents%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    32
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    33
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    34
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    35
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    36
The \indexdef{}{tool}{display}\hypertarget{tool.display}{\hyperlink{tool.display}{\mbox{\isa{\isatool{display}}}}} tool displays documents in DVI or PDF
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    37
  format:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    38
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    39
Usage: isabelle display [OPTIONS] FILE
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    40
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    41
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    42
    -c           cleanup -- remove FILE after use
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    43
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    44
  Display document FILE (in DVI format).
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    45
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    46
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    47
  \medskip The \verb|-c| option causes the input file to be
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    48
  removed after use.  The program for viewing \verb|dvi| files is
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
    49
  determined by the \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    50
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    51
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    52
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    53
\isamarkupsection{Viewing documentation \label{sec:tool-doc}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    54
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    55
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    56
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    57
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    58
The \indexdef{}{tool}{doc}\hypertarget{tool.doc}{\hyperlink{tool.doc}{\mbox{\isa{\isatool{doc}}}}} tool displays online documentation:
28224
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 doc [DOC]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    61
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    62
  View Isabelle documentation DOC, or show list of available documents.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    63
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    64
  If called without arguments, it lists all available documents. Each
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    65
  line starts with an identifier, followed by a short description. Any
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    66
  of these identifiers may be specified as the first argument in order
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    67
  to have the corresponding document displayed.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    68
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
    69
  \medskip The \hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCS}}}} setting specifies the list of
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    70
  directories (separated by colons) to be scanned for documentations.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    71
  The program for viewing \verb|dvi| files is determined by the
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
    72
  \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    73
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    74
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    75
%
47828
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    76
\isamarkupsection{Shell commands within the settings environment \label{sec:tool-env}%
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    77
}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    78
\isamarkuptrue%
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    79
%
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    80
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    81
The \indexdef{}{tool}{env}\hypertarget{tool.env}{\hyperlink{tool.env}{\mbox{\isa{\isatool{env}}}}} tool is a direct wrapper for the standard
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    82
  \verb|/usr/bin/env| command on POSIX systems, running within
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    83
  the Isabelle settings environment (\secref{sec:settings}).
47828
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    84
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    85
  The command-line arguments are that of the underlying version of
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    86
  \verb|env|.  For example, the following invokes an instance of
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    87
  the GNU Bash shell within the Isabelle environment:
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    88
\begin{alltt}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    89
  isabelle env bash
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    90
\end{alltt}%
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    91
\end{isamarkuptext}%
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    92
\isamarkuptrue%
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
    93
%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    94
\isamarkupsection{Getting logic images%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    95
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    96
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    97
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    98
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    99
The \indexdef{}{tool}{findlogics}\hypertarget{tool.findlogics}{\hyperlink{tool.findlogics}{\mbox{\isa{\isatool{findlogics}}}}} tool traverses all directories
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   100
  specified in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}}, looking for Isabelle logic
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   101
  images. Its usage is:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   102
\begin{ttbox}
48577
wenzelm
parents: 47828
diff changeset
   103
Usage: isabelle findlogics
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   104
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   105
  Collect heap file names from ISABELLE_PATH.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   106
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   107
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   108
  The base names of all files found on the path are printed --- sorted
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   109
  and with duplicates removed. Also note that lookup in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}} includes the current values of \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}}
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   110
  and \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}. Thus switching to another ML compiler
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   111
  may change the set of logic images available.%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   112
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   113
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   114
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   115
\isamarkupsection{Inspecting the settings environment \label{sec:tool-getenv}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   116
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   117
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   118
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   119
\begin{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   120
The Isabelle settings environment --- as provided by the
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   121
  site-default and user-specific settings files --- can be inspected
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   122
  with the \indexdef{}{tool}{getenv}\hypertarget{tool.getenv}{\hyperlink{tool.getenv}{\mbox{\isa{\isatool{getenv}}}}} tool:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   123
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   124
Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   125
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   126
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   127
    -a           display complete environment
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   128
    -b           print values only (doesn't work for -a)
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   129
    -d FILE      dump complete environment to FILE
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   130
                 (null terminated entries)
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   131
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   132
  Get value of VARNAMES from the Isabelle settings.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   133
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   134
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   135
  With the \verb|-a| option, one may inspect the full process
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   136
  environment that Isabelle related programs are run in. This usually
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   137
  contains much more variables than are actually Isabelle settings.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   138
  Normally, output is a list of lines of the form \isa{name}\verb|=|\isa{value}. The \verb|-b| option
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   139
  causes only the values to be printed.
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   140
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   141
  Option \verb|-d| produces a dump of the complete environment
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   142
  to the specified file.  Entries are terminated by the ASCII null
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   143
  character, i.e.\ the C string terminator.%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   144
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   145
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   146
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   147
\isamarkupsubsubsection{Examples%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   148
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   149
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   150
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   151
\begin{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   152
Get the ML system name and the location where the compiler binaries
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   153
  are supposed to reside as follows:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   154
\begin{ttbox}
28505
f98751bd715f updated generated file;
wenzelm
parents: 28253
diff changeset
   155
isabelle getenv ML_SYSTEM ML_HOME
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   156
{\out ML_SYSTEM=polyml}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   157
{\out ML_HOME=/usr/share/polyml/x86-linux}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   158
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   159
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   160
  The next one peeks at the output directory for Isabelle logic
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   161
  images:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   162
\begin{ttbox}
28505
f98751bd715f updated generated file;
wenzelm
parents: 28253
diff changeset
   163
isabelle getenv -b ISABELLE_OUTPUT
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   164
{\out /home/me/isabelle/heaps/polyml_x86-linux}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   165
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   166
  Here we have used the \verb|-b| option to suppress the
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   167
  \verb|ISABELLE_OUTPUT=| prefix.  The value above is what
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   168
  became of the following assignment in the default settings file:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   169
\begin{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   170
ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   171
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   172
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   173
  Note how the \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}} value got appended
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   174
  automatically to each path component. This is a special feature of
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   175
  \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}}.%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   176
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   177
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   178
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   179
\isamarkupsection{Installing standalone Isabelle executables \label{sec:tool-install}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   180
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   181
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   182
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   183
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   184
By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} etc.)  are just run from their location within the
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   185
  distribution directory, probably indirectly by the shell through its
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   186
  \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}.  Other schemes of installation are supported by the
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   187
  \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatool{install}}}}} tool:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   188
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   189
Usage: isabelle install [OPTIONS]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   190
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   191
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   192
    -d DISTDIR   use DISTDIR as Isabelle distribution
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   193
                 (default ISABELLE_HOME)
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   194
    -p DIR       install standalone binaries in DIR
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   195
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   196
  Install Isabelle executables with absolute references to the current
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   197
  distribution directory.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   198
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   199
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   200
  The \verb|-d| option overrides the current Isabelle
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   201
  distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   202
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   203
  The \verb|-p| option installs executable wrapper scripts for
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   204
  \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}},
28238
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28224
diff changeset
   205
  \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28224
diff changeset
   206
  Isabelle distribution directory.  A typical \verb|DIR|
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28224
diff changeset
   207
  specification would be some directory expected to be in the shell's
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28224
diff changeset
   208
  \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}, such as \verb|/usr/local/bin|.  It is
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28224
diff changeset
   209
  important to note that a plain manual copy of the original Isabelle
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28224
diff changeset
   210
  executables does not work, since it disrupts the integrity of the
398bf960d3d4 misc tuning and modernization;
wenzelm
parents: 28224
diff changeset
   211
  Isabelle distribution.%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   212
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   213
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   214
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   215
\isamarkupsection{Creating instances of the Isabelle logo%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   216
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   217
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   218
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   219
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   220
The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatool{logo}}}}} tool creates any instance of the generic
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   221
  Isabelle logo as an Encapsuled Postscript file (EPS):
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   222
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   223
Usage: isabelle logo [OPTIONS] NAME
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   225
  Create instance NAME of the Isabelle logo (as EPS).
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   226
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   227
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   228
    -o OUTFILE   set output file (default determined from NAME)
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   229
    -q           quiet mode
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   230
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   231
  You are encouraged to use this to create a derived logo for your
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   232
  Isabelle project.  For example, \hyperlink{tool.logo}{\mbox{\isa{\isatool{logo}}}}~\verb|Bali|
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   233
  creates \verb|isabelle_bali.eps|.%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   234
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   235
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   236
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   237
\isamarkupsection{Isabelle's version of make \label{sec:tool-make}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   238
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   239
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   240
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   241
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   242
The \indexdef{}{tool}{make}\hypertarget{tool.make}{\hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}}} tool is a very simple wrapper for
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   243
  ordinary Unix \hyperlink{executable.make}{\mbox{\isa{\isatt{make}}}}:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   244
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   245
Usage: isabelle make [ARGS ...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   246
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   247
  Compile the logic in current directory using IsaMakefile.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   248
  ARGS are directly passed to the system make program.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   249
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   250
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   251
  Note that the Isabelle settings environment is also active. Thus one
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   252
  may refer to its values within the \verb|IsaMakefile|, e.g.\
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   253
  \verb|$(ISABELLE_OUTPUT)|. Furthermore, programs started from
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   254
  the make file also inherit this environment.  Typically, \verb|IsaMakefile|s defer the real work to \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   255
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   256
  \medskip The basic \verb|IsaMakefile| convention is that the
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   257
  default target builds the actual logic, including its parents if
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   258
  appropriate.  The \verb|images| target is intended to build all
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   259
  local logic images, while the \verb|test| target shall build
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   260
  all related examples.  The \verb|all| target shall do
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   261
  \verb|images| and \verb|test|.%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   262
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   263
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   264
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   265
\isamarkupsection{Printing documents%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   266
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   267
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   268
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   269
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   270
The \indexdef{}{tool}{print}\hypertarget{tool.print}{\hyperlink{tool.print}{\mbox{\isa{\isatool{print}}}}} tool prints documents:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   271
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   272
Usage: isabelle print [OPTIONS] FILE
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   273
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   274
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   275
    -c           cleanup -- remove FILE after use
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   276
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   277
  Print document FILE.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   278
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   279
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   280
  The \verb|-c| option causes the input file to be removed
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   281
  after use.  The printer spool command is determined by the \hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isaliteral{5F}{\isacharunderscore}}COMMAND}}}} setting.%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   282
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   283
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   284
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   285
\isamarkupsection{Remove awkward symbol names from theory sources%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   286
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   287
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   288
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   289
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   290
The \indexdef{}{tool}{unsymbolize}\hypertarget{tool.unsymbolize}{\hyperlink{tool.unsymbolize}{\mbox{\isa{\isatool{unsymbolize}}}}} tool tunes Isabelle theory sources to
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   291
  improve readability for plain ASCII output (e.g.\ in email
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   292
  communication).  Most notably, \hyperlink{tool.unsymbolize}{\mbox{\isa{\isatool{unsymbolize}}}} replaces awkward
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   293
  arrow symbols such as \verb|\|\verb|<Longrightarrow>|
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   294
  by \verb|==>|.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   295
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   296
Usage: isabelle unsymbolize [FILES|DIRS...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   297
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   298
  Recursively find .thy/.ML files, removing unreadable symbol names.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   299
  Note: this is an ad-hoc script; there is no systematic way to replace
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   300
  symbols independently of the inner syntax of a theory!
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   301
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   302
  Renames old versions of FILES by appending "~~".
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   303
\end{ttbox}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   304
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   305
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   306
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   307
\isamarkupsection{Output the version identifier of the Isabelle distribution%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   308
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   309
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   310
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   311
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   312
The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatool{version}}}}} tool displays Isabelle version information:
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   313
\begin{ttbox}
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   314
Usage: isabelle version [OPTIONS]
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   315
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   316
  Options are:
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   317
    -i           short identification (derived from Mercurial id)
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   318
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   319
  Display Isabelle version information.
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   320
\end{ttbox}
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   321
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   322
  \medskip The default is to output the full version string of the
47827
13530d774a21 updated system manual for release;
wenzelm
parents: 44799
diff changeset
   323
  Isabelle distribution, e.g.\ ``\verb|Isabelle2012: May 2012|.
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   324
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   325
  The \verb|-i| option produces a short identification derived
2fe62d602681 isabelle version -i;
wenzelm
parents: 40802
diff changeset
   326
  from the Mercurial id of the \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} directory.%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   327
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   328
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   329
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   330
\isamarkupsection{Convert XML to YXML%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   331
}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   332
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   333
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   334
\begin{isamarkuptext}%
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   335
The \indexdef{}{tool}{yxml}\hypertarget{tool.yxml}{\hyperlink{tool.yxml}{\mbox{\isa{\isatool{yxml}}}}} tool converts a standard XML document (stdin)
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   336
  to the much simpler and more efficient YXML format of Isabelle
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   337
  (stdout).  The YXML format is defined as follows.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   338
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   339
  \begin{enumerate}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   340
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   341
  \item The encoding is always UTF-8.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   342
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   343
  \item Body text is represented verbatim (no escaping, no special
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   344
  treatment of white space, no named entities, no CDATA chunks, no
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   345
  comments).
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   346
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   347
  \item Markup elements are represented via ASCII control characters
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   348
  \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{5}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{6}}{\isaliteral{22}{\isachardoublequote}}} as follows:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   349
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   350
  \begin{tabular}{ll}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   351
    XML & YXML \\\hline
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   352
    \verb|<|\isa{{\isaliteral{22}{\isachardoublequote}}name\ attribute{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}\verb|>| &
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   353
    \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Yname\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Yattribute{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value{\isaliteral{5C3C646F74733E}{\isasymdots}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} \\
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   354
    \verb|</|\isa{name}\verb|>| & \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} \\
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   355
  \end{tabular}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   356
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   357
  There is no special case for empty body text, i.e.\ \verb|<foo/>| is treated like \verb|<foo></foo>|.  Also note that
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   358
  \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}} may never occur in
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   359
  well-formed XML documents.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   360
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   361
  \end{enumerate}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   362
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   363
  Parsing YXML is pretty straight-forward: split the text into chunks
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   364
  separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}}, then split each chunk into
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   365
  sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.  Markup chunks start
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   366
  with an empty sub-chunk, and a second empty sub-chunk indicates
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   367
  close of an element.  Any other non-empty chunk consists of plain
44799
1fd0a1276a09 updated file locations;
wenzelm
parents: 43564
diff changeset
   368
  text.  For example, see \verb|~~/src/Pure/PIDE/yxml.ML| or
1fd0a1276a09 updated file locations;
wenzelm
parents: 43564
diff changeset
   369
  \verb|~~/src/Pure/PIDE/yxml.scala|.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   370
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   371
  YXML documents may be detected quickly by checking that the first
40406
313a24b66a8d updated generated files;
wenzelm
parents: 32325
diff changeset
   372
  two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   373
\end{isamarkuptext}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   374
\isamarkuptrue%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   375
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   376
\isadelimtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   377
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   378
\endisadelimtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   379
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   380
\isatagtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   381
\isacommand{end}\isamarkupfalse%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   382
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   383
\endisatagtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   384
{\isafoldtheory}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   385
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   386
\isadelimtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   387
%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   388
\endisadelimtheory
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   389
\end{isabellebody}%
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   390
%%% Local Variables:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   391
%%% mode: latex
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   392
%%% TeX-master: "root"
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   393
%%% End: