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