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