converted misc.tex;
authorwenzelm
Mon Sep 15 20:22:38 2008 +0200 (2008-09-15 ago)
changeset 2822410487d954a8f
parent 28223 eee194395fdc
child 28225 5d1fc22bccdf
converted misc.tex;
doc-src/System/IsaMakefile
doc-src/System/Makefile
doc-src/System/Thy/Misc.thy
doc-src/System/Thy/ROOT.ML
doc-src/System/Thy/document/Misc.tex
doc-src/System/misc.tex
doc-src/System/system.tex
     1.1 --- a/doc-src/System/IsaMakefile	Mon Sep 15 19:43:10 2008 +0200
     1.2 +++ b/doc-src/System/IsaMakefile	Mon Sep 15 20:22:38 2008 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  Pure-System: $(LOG)/Pure-System.gz
     1.5  
     1.6  $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML	\
     1.7 -  Thy/Basics.thy Thy/Presentation.thy
     1.8 +  Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy
     1.9  	@$(USEDIR) -s System Pure Thy
    1.10  
    1.11  
     2.1 --- a/doc-src/System/Makefile	Mon Sep 15 19:43:10 2008 +0200
     2.2 +++ b/doc-src/System/Makefile	Mon Sep 15 20:22:38 2008 +0200
     2.3 @@ -12,9 +12,9 @@
     2.4  include ../Makefile.in
     2.5  
     2.6  NAME = system
     2.7 -FILES = system.tex Thy/document/Basics.tex misc.tex		\
     2.8 -	Thy/document/Presentation.tex symbols.tex ../iman.sty	\
     2.9 -	../extra.sty ../ttbox.sty ../manual.bib
    2.10 +FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \
    2.11 +	Thy/document/Presentation.tex symbols.tex ../iman.sty	 \
    2.12 +	../extra.sty ../ttbox.sty ../manual.bib			 \
    2.13  
    2.14  OUTPUT = syms.tex
    2.15  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/System/Thy/Misc.thy	Mon Sep 15 20:22:38 2008 +0200
     3.3 @@ -0,0 +1,353 @@
     3.4 +(* $Id$ *)
     3.5 +
     3.6 +theory Misc
     3.7 +imports Pure
     3.8 +begin
     3.9 +
    3.10 +chapter {* Miscellaneous tools \label{ch:tools} *}
    3.11 +
    3.12 +text {*
    3.13 +  Subsequently we describe various Isabelle related utilities, given
    3.14 +  in alphabetical order.
    3.15 +*}
    3.16 +
    3.17 +
    3.18 +section {* Displaying documents *}
    3.19 +
    3.20 +text {*
    3.21 +  The @{tool_def display} utility displays documents in DVI or PDF
    3.22 +  format:
    3.23 +\begin{ttbox}
    3.24 +Usage: display [OPTIONS] FILE
    3.25 +
    3.26 +  Options are:
    3.27 +    -c           cleanup -- remove FILE after use
    3.28 +
    3.29 +  Display document FILE (in DVI format).
    3.30 +\end{ttbox}
    3.31 +
    3.32 +  \medskip The @{verbatim "-c"} option causes the input file to be
    3.33 +  removed after use.  The program for viewing @{verbatim dvi} files is
    3.34 +  determined by the @{setting DVI_VIEWER} setting.
    3.35 +*}
    3.36 +
    3.37 +
    3.38 +section {* Viewing documentation \label{sec:tool-doc} *}
    3.39 +
    3.40 +text {*
    3.41 +  The @{tool_def doc} utility displays online documentation:
    3.42 +\begin{ttbox}
    3.43 +Usage: doc [DOC]
    3.44 +
    3.45 +  View Isabelle documentation DOC, or show list of available documents.
    3.46 +\end{ttbox}
    3.47 +  If called without arguments, it lists all available documents. Each
    3.48 +  line starts with an identifier, followed by a short description. Any
    3.49 +  of these identifiers may be specified as the first argument in order
    3.50 +  to have the corresponding document displayed.
    3.51 +
    3.52 +  \medskip The @{setting ISABELLE_DOCS} setting specifies the list of
    3.53 +  directories (separated by colons) to be scanned for documentations.
    3.54 +  The program for viewing @{verbatim dvi} files is determined by the
    3.55 +  @{setting DVI_VIEWER} setting.
    3.56 +*}
    3.57 +
    3.58 +
    3.59 +section {* Getting logic images *}
    3.60 +
    3.61 +text {*
    3.62 +  The @{tool_def findlogics} utility traverses all directories
    3.63 +  specified in @{setting ISABELLE_PATH}, looking for Isabelle logic
    3.64 +  images. Its usage is:
    3.65 +\begin{ttbox}
    3.66 +Usage: findlogics
    3.67 +
    3.68 +  Collect heap file names from ISABELLE_PATH.
    3.69 +\end{ttbox}
    3.70 +
    3.71 +  The base names of all files found on the path are printed --- sorted
    3.72 +  and with duplicates removed. Also note that lookup in @{setting
    3.73 +  ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM}
    3.74 +  and @{setting ML_PLATFORM}. Thus switching to another ML compiler
    3.75 +  may change the set of logic images available.
    3.76 +*}
    3.77 +
    3.78 +
    3.79 +section {* Inspecting the settings environment \label{sec:tool-getenv} *}
    3.80 +
    3.81 +text {*
    3.82 +  The Isabelle settings environment --- as provided by the
    3.83 +  site-default and user-specific settings files --- can be inspected
    3.84 +  with the @{tool_def getenv} utility:
    3.85 +\begin{ttbox}
    3.86 +Usage: getenv [OPTIONS] [VARNAMES ...]
    3.87 +
    3.88 +  Options are:
    3.89 +    -a           display complete environment
    3.90 +    -b           print values only (doesn't work for -a)
    3.91 +
    3.92 +  Get value of VARNAMES from the Isabelle settings.
    3.93 +\end{ttbox}
    3.94 +
    3.95 +  With the @{verbatim "-a"} option, one may inspect the full process
    3.96 +  environment that Isabelle related programs are run in. This usually
    3.97 +  contains much more variables than are actually Isabelle settings.
    3.98 +  Normally, output is a list of lines of the form @{text
    3.99 +  name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option
   3.100 +  causes only the values to be printed.
   3.101 +*}
   3.102 +
   3.103 +
   3.104 +subsubsection {* Examples *}
   3.105 +
   3.106 +text {*
   3.107 +  Get the ML system name and the location where the compiler binaries
   3.108 +  are supposed to reside as follows:
   3.109 +\begin{ttbox}
   3.110 +isatool getenv ML_SYSTEM ML_HOME
   3.111 +{\out ML_SYSTEM=polyml}
   3.112 +{\out ML_HOME=/usr/share/polyml/x86-linux}
   3.113 +\end{ttbox}
   3.114 +
   3.115 +  The next one peeks at the output directory for Isabelle logic
   3.116 +  images:
   3.117 +\begin{ttbox}
   3.118 +isatool getenv -b ISABELLE_OUTPUT
   3.119 +{\out /home/me/isabelle/heaps/polyml_x86-linux}
   3.120 +\end{ttbox}
   3.121 +  Here we have used the @{verbatim "-b"} option to suppress the
   3.122 +  @{verbatim "ISABELLE_OUTPUT="} prefix.  The value above is what
   3.123 +  became of the following assignment in the default settings file:
   3.124 +\begin{ttbox}
   3.125 +ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
   3.126 +\end{ttbox}
   3.127 +
   3.128 +  Note how the @{setting ML_IDENTIFIER} value got appended
   3.129 +  automatically to each path component. This is a special feature of
   3.130 +  @{setting ISABELLE_OUTPUT}.
   3.131 +*}
   3.132 +
   3.133 +
   3.134 +section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
   3.135 +
   3.136 +text {*
   3.137 +  By default, the Isabelle binaries (@{executable isabelle},
   3.138 +  @{executable isatool} etc.) are just run from their location within
   3.139 +  the distribution directory, probably indirectly by the shell through
   3.140 +  its @{verbatim PATH}.  Other schemes of installation are supported
   3.141 +  by the @{tool_def install} utility:
   3.142 +\begin{ttbox}
   3.143 +Usage: install [OPTIONS]
   3.144 +
   3.145 +  Options are:
   3.146 +    -d DISTDIR   use DISTDIR as Isabelle distribution
   3.147 +                 (default ISABELLE_HOME)
   3.148 +    -p DIR       install standalone binaries in DIR
   3.149 +
   3.150 +  Install Isabelle executables with absolute references to the current
   3.151 +  distribution directory.
   3.152 +\end{ttbox}
   3.153 +
   3.154 +  The @{verbatim "-d"} option overrides the current Isabelle
   3.155 +  distribution directory as determined by @{setting ISABELLE_HOME}.
   3.156 +
   3.157 +  The @{verbatim "-p"} option installs executable wrapper scripts for
   3.158 +  @{executable isabelle}, @{executable isatool}, @{executable
   3.159 +  Isabelle}, containing proper absolute references to the Isabelle
   3.160 +  distribution directory.  A typical @{verbatim DIR} specification
   3.161 +  would be some directory expected to be in the shell's @{verbatim
   3.162 +  PATH}, such as @{verbatim "/usr/local/bin"}.  It is important to
   3.163 +  note that a plain manual copy of the original Isabelle executables
   3.164 +  does not work, since it disrupts the integrity of the Isabelle
   3.165 +  distribution.
   3.166 +*}
   3.167 +
   3.168 +
   3.169 +section {* Creating instances of the Isabelle logo *}
   3.170 +
   3.171 +text {*
   3.172 +  The @{tool_def logo} utility creates any instance of the generic
   3.173 +  Isabelle logo as an Encapsuled Postscript file (EPS):
   3.174 +\begin{ttbox}
   3.175 +Usage: logo [OPTIONS] NAME
   3.176 +
   3.177 +  Create instance NAME of the Isabelle logo (as EPS).
   3.178 +
   3.179 +  Options are:
   3.180 +    -o OUTFILE   set output file (default determined from NAME)
   3.181 +    -q           quiet mode
   3.182 +\end{ttbox}
   3.183 +  You are encouraged to use this to create a derived logo for your
   3.184 +  Isabelle project.  For example, @{verbatim "isatool logo Bali"}
   3.185 +  creates @{verbatim isabelle_bali.eps}.
   3.186 +*}
   3.187 +
   3.188 +
   3.189 +section {* Isabelle's version of make \label{sec:tool-make} *}
   3.190 +
   3.191 +text {*
   3.192 +  The Isabelle @{tool_def make} utility is a very simple wrapper for
   3.193 +  ordinary Unix @{executable make}:
   3.194 +\begin{ttbox}
   3.195 +Usage: make [ARGS ...]
   3.196 +
   3.197 +  Compile the logic in current directory using IsaMakefile.
   3.198 +  ARGS are directly passed to the system make program.
   3.199 +\end{ttbox}
   3.200 +
   3.201 +  Note that the Isabelle settings environment is also active. Thus one
   3.202 +  may refer to its values within the @{verbatim IsaMakefile}, e.g.\
   3.203 +  @{verbatim "$(ISABELLE_OUTPUT)"}. Furthermore, programs started from
   3.204 +  the make file also inherit this environment.  Typically, @{verbatim
   3.205 +  IsaMakefile}s defer the real work to the @{tool_ref usedir} utility.
   3.206 +
   3.207 +  \medskip The basic @{verbatim IsaMakefile} convention is that the
   3.208 +  default target builds the actual logic, including its parents if
   3.209 +  appropriate.  The @{verbatim images} target is intended to build all
   3.210 +  local logic images, while the @{verbatim test} target shall build
   3.211 +  all related examples.  The @{verbatim all} target shall do
   3.212 +  @{verbatim images} and @{verbatim test}.
   3.213 +*}
   3.214 +
   3.215 +
   3.216 +subsubsection {* Examples *}
   3.217 +
   3.218 +text {*
   3.219 +  Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
   3.220 +  object-logics as a model for your own developments.  For example,
   3.221 +  see @{verbatim "src/FOL/IsaMakefile"}.
   3.222 +*}
   3.223 +
   3.224 +
   3.225 +section {* Make all logics *}
   3.226 +
   3.227 +text {*
   3.228 +  The @{tool_def makeall} utility applies Isabelle make to all logic
   3.229 +  directories of the distribution:
   3.230 +\begin{ttbox}
   3.231 +Usage: makeall [ARGS ...]
   3.232 +
   3.233 +  Apply isatool make to all logics (passing ARGS).
   3.234 +\end{ttbox}
   3.235 +
   3.236 +  The arguments @{verbatim ARGS} are just passed verbatim to each
   3.237 +  @{tool make} invocation.
   3.238 +*}
   3.239 +
   3.240 +
   3.241 +section {* Printing documents *}
   3.242 +
   3.243 +text {*
   3.244 +  The @{tool_def print} utility prints documents:
   3.245 +\begin{ttbox}
   3.246 +Usage: print [OPTIONS] FILE
   3.247 +
   3.248 +  Options are:
   3.249 +    -c           cleanup -- remove FILE after use
   3.250 +
   3.251 +  Print document FILE.
   3.252 +\end{ttbox}
   3.253 +
   3.254 +  The @{verbatim "-c"} option causes the input file to be removed
   3.255 +  after use.  The printer spool command is determined by the @{setting
   3.256 +  PRINT_COMMAND} setting.
   3.257 +*}
   3.258 +
   3.259 +
   3.260 +section {* Run Isabelle with plain tty interaction \label{sec:tool-tty} *}
   3.261 +
   3.262 +text {*
   3.263 +  The @{tool_def tty} utility runs the Isabelle process interactively
   3.264 +  within a plain terminal session:
   3.265 +\begin{ttbox}
   3.266 +Usage: tty [OPTIONS]
   3.267 +
   3.268 +  Options are:
   3.269 +    -l NAME      logic image name (default ISABELLE_LOGIC)
   3.270 +    -m MODE      add print mode for output
   3.271 +    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
   3.272 +
   3.273 +  Run Isabelle process with plain tty interaction, and optional line editor.
   3.274 +\end{ttbox}
   3.275 +
   3.276 +  The @{verbatim "-l"} option specifies the logic image.  The
   3.277 +  @{verbatim "-m"} option specifies additional print modes.  The The
   3.278 +  @{verbatim "-p"} option specifies an alternative line editor (such
   3.279 +  as the @{executable rlwrap} wrapper for GNU readline); the fall-back
   3.280 +  is to use raw standard input.
   3.281 +*}
   3.282 +
   3.283 +
   3.284 +section {* Remove awkward symbol names from theory sources *}
   3.285 +
   3.286 +text {*
   3.287 +  The @{tool_def unsymbolize} utility tunes Isabelle theory sources to
   3.288 +  improve readability for plain ASCII output (e.g.\ in email
   3.289 +  communication).  Most notably, @{tool unsymbolize} replaces awkward
   3.290 +  arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
   3.291 +  by @{verbatim "==>"}.
   3.292 +\begin{ttbox}
   3.293 +Usage: unsymbolize [FILES|DIRS...]
   3.294 +
   3.295 +  Recursively find .thy/.ML files, removing unreadable symbol names.
   3.296 +  Note: this is an ad-hoc script; there is no systematic way to replace
   3.297 +  symbols independently of the inner syntax of a theory!
   3.298 +
   3.299 +  Renames old versions of FILES by appending "~~".
   3.300 +\end{ttbox}
   3.301 +*}
   3.302 +
   3.303 +
   3.304 +section {* Output the version identifier of the Isabelle distribution *}
   3.305 +
   3.306 +text {*
   3.307 +  The @{tool_def version} utility outputs the full version string of
   3.308 +  the Isabelle distribution being used, e.g.\ ``@{verbatim
   3.309 +  "Isabelle2008: June 2008"}.  There are no options nor arguments.
   3.310 +*}
   3.311 +
   3.312 +
   3.313 +section {* Convert XML to YXML *}
   3.314 +
   3.315 +text {*
   3.316 +  The @{tool_def yxml} tool converts a standard XML document (stdin)
   3.317 +  to the much simpler and more efficient YXML format of Isabelle
   3.318 +  (stdout).  The YXML format is defined as follows.
   3.319 +
   3.320 +  \begin{enumerate}
   3.321 +
   3.322 +  \item The encoding is always UTF-8.
   3.323 +
   3.324 +  \item Body text is represented verbatim (no escaping, no special
   3.325 +  treatment of white space, no named entities, no CDATA chunks, no
   3.326 +  comments).
   3.327 +
   3.328 +  \item Markup elements are represented via ASCII control characters
   3.329 +  @{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows:
   3.330 +
   3.331 +  \begin{tabular}{ll}
   3.332 +    XML & YXML \\\hline
   3.333 +    @{verbatim "<"}@{text "name attribute"}@{verbatim "="}@{text "value \<dots>"}@{verbatim ">"} &
   3.334 +    @{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\<dots>\<^bold>X"} \\
   3.335 +    @{verbatim "</"}@{text name}@{verbatim ">"} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\
   3.336 +  \end{tabular}
   3.337 +
   3.338 +  There is no special case for empty body text, i.e.\ @{verbatim
   3.339 +  "<foo/>"} is treated like @{verbatim "<foo></foo>"}.  Also note that
   3.340 +  @{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in
   3.341 +  well-formed XML documents.
   3.342 +
   3.343 +  \end{enumerate}
   3.344 +
   3.345 +  Parsing YXML is pretty straight-forward: split the text into chunks
   3.346 +  separated by @{text "\<^bold>X"}, then split each chunk into
   3.347 +  sub-chunks separated by @{text "\<^bold>Y"}.  Markup chunks start
   3.348 +  with an empty sub-chunk, and a second empty sub-chunk indicates
   3.349 +  close of an element.  Any other non-empty chunk consists of plain
   3.350 +  text.
   3.351 +
   3.352 +  YXML documents may be detected quickly by checking that the first
   3.353 +  two characters are @{text "\<^bold>X\<^bold>Y"}.
   3.354 +*}
   3.355 +
   3.356 +end
   3.357 \ No newline at end of file
     4.1 --- a/doc-src/System/Thy/ROOT.ML	Mon Sep 15 19:43:10 2008 +0200
     4.2 +++ b/doc-src/System/Thy/ROOT.ML	Mon Sep 15 20:22:38 2008 +0200
     4.3 @@ -6,3 +6,4 @@
     4.4  
     4.5  use_thy "Basics";
     4.6  use_thy "Presentation";
     4.7 +use_thy "Misc";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/System/Thy/document/Misc.tex	Mon Sep 15 20:22:38 2008 +0200
     5.3 @@ -0,0 +1,411 @@
     5.4 +%
     5.5 +\begin{isabellebody}%
     5.6 +\def\isabellecontext{Misc}%
     5.7 +%
     5.8 +\isadelimtheory
     5.9 +\isanewline
    5.10 +\isanewline
    5.11 +%
    5.12 +\endisadelimtheory
    5.13 +%
    5.14 +\isatagtheory
    5.15 +\isacommand{theory}\isamarkupfalse%
    5.16 +\ Misc\isanewline
    5.17 +\isakeyword{imports}\ Pure\isanewline
    5.18 +\isakeyword{begin}%
    5.19 +\endisatagtheory
    5.20 +{\isafoldtheory}%
    5.21 +%
    5.22 +\isadelimtheory
    5.23 +%
    5.24 +\endisadelimtheory
    5.25 +%
    5.26 +\isamarkupchapter{Miscellaneous tools \label{ch:tools}%
    5.27 +}
    5.28 +\isamarkuptrue%
    5.29 +%
    5.30 +\begin{isamarkuptext}%
    5.31 +Subsequently we describe various Isabelle related utilities, given
    5.32 +  in alphabetical order.%
    5.33 +\end{isamarkuptext}%
    5.34 +\isamarkuptrue%
    5.35 +%
    5.36 +\isamarkupsection{Displaying documents%
    5.37 +}
    5.38 +\isamarkuptrue%
    5.39 +%
    5.40 +\begin{isamarkuptext}%
    5.41 +The \indexdef{}{tool}{display}\hypertarget{tool.display}{\hyperlink{tool.display}{\mbox{\isa{\isatt{display}}}}} utility displays documents in DVI or PDF
    5.42 +  format:
    5.43 +\begin{ttbox}
    5.44 +Usage: display [OPTIONS] FILE
    5.45 +
    5.46 +  Options are:
    5.47 +    -c           cleanup -- remove FILE after use
    5.48 +
    5.49 +  Display document FILE (in DVI format).
    5.50 +\end{ttbox}
    5.51 +
    5.52 +  \medskip The \verb|-c| option causes the input file to be
    5.53 +  removed after use.  The program for viewing \verb|dvi| files is
    5.54 +  determined by the \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isacharunderscore}VIEWER}}}} setting.%
    5.55 +\end{isamarkuptext}%
    5.56 +\isamarkuptrue%
    5.57 +%
    5.58 +\isamarkupsection{Viewing documentation \label{sec:tool-doc}%
    5.59 +}
    5.60 +\isamarkuptrue%
    5.61 +%
    5.62 +\begin{isamarkuptext}%
    5.63 +The \indexdef{}{tool}{doc}\hypertarget{tool.doc}{\hyperlink{tool.doc}{\mbox{\isa{\isatt{doc}}}}} utility displays online documentation:
    5.64 +\begin{ttbox}
    5.65 +Usage: doc [DOC]
    5.66 +
    5.67 +  View Isabelle documentation DOC, or show list of available documents.
    5.68 +\end{ttbox}
    5.69 +  If called without arguments, it lists all available documents. Each
    5.70 +  line starts with an identifier, followed by a short description. Any
    5.71 +  of these identifiers may be specified as the first argument in order
    5.72 +  to have the corresponding document displayed.
    5.73 +
    5.74 +  \medskip The \hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DOCS}}}} setting specifies the list of
    5.75 +  directories (separated by colons) to be scanned for documentations.
    5.76 +  The program for viewing \verb|dvi| files is determined by the
    5.77 +  \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isacharunderscore}VIEWER}}}} setting.%
    5.78 +\end{isamarkuptext}%
    5.79 +\isamarkuptrue%
    5.80 +%
    5.81 +\isamarkupsection{Getting logic images%
    5.82 +}
    5.83 +\isamarkuptrue%
    5.84 +%
    5.85 +\begin{isamarkuptext}%
    5.86 +The \indexdef{}{tool}{findlogics}\hypertarget{tool.findlogics}{\hyperlink{tool.findlogics}{\mbox{\isa{\isatt{findlogics}}}}} utility traverses all directories
    5.87 +  specified in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}}, looking for Isabelle logic
    5.88 +  images. Its usage is:
    5.89 +\begin{ttbox}
    5.90 +Usage: findlogics
    5.91 +
    5.92 +  Collect heap file names from ISABELLE_PATH.
    5.93 +\end{ttbox}
    5.94 +
    5.95 +  The base names of all files found on the path are printed --- sorted
    5.96 +  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}}}}
    5.97 +  and \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}}. Thus switching to another ML compiler
    5.98 +  may change the set of logic images available.%
    5.99 +\end{isamarkuptext}%
   5.100 +\isamarkuptrue%
   5.101 +%
   5.102 +\isamarkupsection{Inspecting the settings environment \label{sec:tool-getenv}%
   5.103 +}
   5.104 +\isamarkuptrue%
   5.105 +%
   5.106 +\begin{isamarkuptext}%
   5.107 +The Isabelle settings environment --- as provided by the
   5.108 +  site-default and user-specific settings files --- can be inspected
   5.109 +  with the \indexdef{}{tool}{getenv}\hypertarget{tool.getenv}{\hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}} utility:
   5.110 +\begin{ttbox}
   5.111 +Usage: getenv [OPTIONS] [VARNAMES ...]
   5.112 +
   5.113 +  Options are:
   5.114 +    -a           display complete environment
   5.115 +    -b           print values only (doesn't work for -a)
   5.116 +
   5.117 +  Get value of VARNAMES from the Isabelle settings.
   5.118 +\end{ttbox}
   5.119 +
   5.120 +  With the \verb|-a| option, one may inspect the full process
   5.121 +  environment that Isabelle related programs are run in. This usually
   5.122 +  contains much more variables than are actually Isabelle settings.
   5.123 +  Normally, output is a list of lines of the form \isa{name}\verb|=|\isa{value}. The \verb|-b| option
   5.124 +  causes only the values to be printed.%
   5.125 +\end{isamarkuptext}%
   5.126 +\isamarkuptrue%
   5.127 +%
   5.128 +\isamarkupsubsubsection{Examples%
   5.129 +}
   5.130 +\isamarkuptrue%
   5.131 +%
   5.132 +\begin{isamarkuptext}%
   5.133 +Get the ML system name and the location where the compiler binaries
   5.134 +  are supposed to reside as follows:
   5.135 +\begin{ttbox}
   5.136 +isatool getenv ML_SYSTEM ML_HOME
   5.137 +{\out ML_SYSTEM=polyml}
   5.138 +{\out ML_HOME=/usr/share/polyml/x86-linux}
   5.139 +\end{ttbox}
   5.140 +
   5.141 +  The next one peeks at the output directory for Isabelle logic
   5.142 +  images:
   5.143 +\begin{ttbox}
   5.144 +isatool getenv -b ISABELLE_OUTPUT
   5.145 +{\out /home/me/isabelle/heaps/polyml_x86-linux}
   5.146 +\end{ttbox}
   5.147 +  Here we have used the \verb|-b| option to suppress the
   5.148 +  \verb|ISABELLE_OUTPUT=| prefix.  The value above is what
   5.149 +  became of the following assignment in the default settings file:
   5.150 +\begin{ttbox}
   5.151 +ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
   5.152 +\end{ttbox}
   5.153 +
   5.154 +  Note how the \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} value got appended
   5.155 +  automatically to each path component. This is a special feature of
   5.156 +  \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}.%
   5.157 +\end{isamarkuptext}%
   5.158 +\isamarkuptrue%
   5.159 +%
   5.160 +\isamarkupsection{Installing standalone Isabelle executables \label{sec:tool-install}%
   5.161 +}
   5.162 +\isamarkuptrue%
   5.163 +%
   5.164 +\begin{isamarkuptext}%
   5.165 +By default, the Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}},
   5.166 +  \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} etc.) are just run from their location within
   5.167 +  the distribution directory, probably indirectly by the shell through
   5.168 +  its \verb|PATH|.  Other schemes of installation are supported
   5.169 +  by the \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
   5.170 +\begin{ttbox}
   5.171 +Usage: install [OPTIONS]
   5.172 +
   5.173 +  Options are:
   5.174 +    -d DISTDIR   use DISTDIR as Isabelle distribution
   5.175 +                 (default ISABELLE_HOME)
   5.176 +    -p DIR       install standalone binaries in DIR
   5.177 +
   5.178 +  Install Isabelle executables with absolute references to the current
   5.179 +  distribution directory.
   5.180 +\end{ttbox}
   5.181 +
   5.182 +  The \verb|-d| option overrides the current Isabelle
   5.183 +  distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}.
   5.184 +
   5.185 +  The \verb|-p| option installs executable wrapper scripts for
   5.186 +  \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}, \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}}, \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the Isabelle
   5.187 +  distribution directory.  A typical \verb|DIR| specification
   5.188 +  would be some directory expected to be in the shell's \verb|PATH|, such as \verb|/usr/local/bin|.  It is important to
   5.189 +  note that a plain manual copy of the original Isabelle executables
   5.190 +  does not work, since it disrupts the integrity of the Isabelle
   5.191 +  distribution.%
   5.192 +\end{isamarkuptext}%
   5.193 +\isamarkuptrue%
   5.194 +%
   5.195 +\isamarkupsection{Creating instances of the Isabelle logo%
   5.196 +}
   5.197 +\isamarkuptrue%
   5.198 +%
   5.199 +\begin{isamarkuptext}%
   5.200 +The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}} utility creates any instance of the generic
   5.201 +  Isabelle logo as an Encapsuled Postscript file (EPS):
   5.202 +\begin{ttbox}
   5.203 +Usage: logo [OPTIONS] NAME
   5.204 +
   5.205 +  Create instance NAME of the Isabelle logo (as EPS).
   5.206 +
   5.207 +  Options are:
   5.208 +    -o OUTFILE   set output file (default determined from NAME)
   5.209 +    -q           quiet mode
   5.210 +\end{ttbox}
   5.211 +  You are encouraged to use this to create a derived logo for your
   5.212 +  Isabelle project.  For example, \verb|isatool logo Bali|
   5.213 +  creates \verb|isabelle_bali.eps|.%
   5.214 +\end{isamarkuptext}%
   5.215 +\isamarkuptrue%
   5.216 +%
   5.217 +\isamarkupsection{Isabelle's version of make \label{sec:tool-make}%
   5.218 +}
   5.219 +\isamarkuptrue%
   5.220 +%
   5.221 +\begin{isamarkuptext}%
   5.222 +The Isabelle \indexdef{}{tool}{make}\hypertarget{tool.make}{\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}} utility is a very simple wrapper for
   5.223 +  ordinary Unix \hyperlink{executable.make}{\mbox{\isa{\isatt{make}}}}:
   5.224 +\begin{ttbox}
   5.225 +Usage: make [ARGS ...]
   5.226 +
   5.227 +  Compile the logic in current directory using IsaMakefile.
   5.228 +  ARGS are directly passed to the system make program.
   5.229 +\end{ttbox}
   5.230 +
   5.231 +  Note that the Isabelle settings environment is also active. Thus one
   5.232 +  may refer to its values within the \verb|IsaMakefile|, e.g.\
   5.233 +  \verb|$(ISABELLE_OUTPUT)|. Furthermore, programs started from
   5.234 +  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.
   5.235 +
   5.236 +  \medskip The basic \verb|IsaMakefile| convention is that the
   5.237 +  default target builds the actual logic, including its parents if
   5.238 +  appropriate.  The \verb|images| target is intended to build all
   5.239 +  local logic images, while the \verb|test| target shall build
   5.240 +  all related examples.  The \verb|all| target shall do
   5.241 +  \verb|images| and \verb|test|.%
   5.242 +\end{isamarkuptext}%
   5.243 +\isamarkuptrue%
   5.244 +%
   5.245 +\isamarkupsubsubsection{Examples%
   5.246 +}
   5.247 +\isamarkuptrue%
   5.248 +%
   5.249 +\begin{isamarkuptext}%
   5.250 +Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
   5.251 +  object-logics as a model for your own developments.  For example,
   5.252 +  see \verb|src/FOL/IsaMakefile|.%
   5.253 +\end{isamarkuptext}%
   5.254 +\isamarkuptrue%
   5.255 +%
   5.256 +\isamarkupsection{Make all logics%
   5.257 +}
   5.258 +\isamarkuptrue%
   5.259 +%
   5.260 +\begin{isamarkuptext}%
   5.261 +The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatt{makeall}}}}} utility applies Isabelle make to all logic
   5.262 +  directories of the distribution:
   5.263 +\begin{ttbox}
   5.264 +Usage: makeall [ARGS ...]
   5.265 +
   5.266 +  Apply isatool make to all logics (passing ARGS).
   5.267 +\end{ttbox}
   5.268 +
   5.269 +  The arguments \verb|ARGS| are just passed verbatim to each
   5.270 +  \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} invocation.%
   5.271 +\end{isamarkuptext}%
   5.272 +\isamarkuptrue%
   5.273 +%
   5.274 +\isamarkupsection{Printing documents%
   5.275 +}
   5.276 +\isamarkuptrue%
   5.277 +%
   5.278 +\begin{isamarkuptext}%
   5.279 +The \indexdef{}{tool}{print}\hypertarget{tool.print}{\hyperlink{tool.print}{\mbox{\isa{\isatt{print}}}}} utility prints documents:
   5.280 +\begin{ttbox}
   5.281 +Usage: print [OPTIONS] FILE
   5.282 +
   5.283 +  Options are:
   5.284 +    -c           cleanup -- remove FILE after use
   5.285 +
   5.286 +  Print document FILE.
   5.287 +\end{ttbox}
   5.288 +
   5.289 +  The \verb|-c| option causes the input file to be removed
   5.290 +  after use.  The printer spool command is determined by the \hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isacharunderscore}COMMAND}}}} setting.%
   5.291 +\end{isamarkuptext}%
   5.292 +\isamarkuptrue%
   5.293 +%
   5.294 +\isamarkupsection{Run Isabelle with plain tty interaction \label{sec:tool-tty}%
   5.295 +}
   5.296 +\isamarkuptrue%
   5.297 +%
   5.298 +\begin{isamarkuptext}%
   5.299 +The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} utility runs the Isabelle process interactively
   5.300 +  within a plain terminal session:
   5.301 +\begin{ttbox}
   5.302 +Usage: tty [OPTIONS]
   5.303 +
   5.304 +  Options are:
   5.305 +    -l NAME      logic image name (default ISABELLE_LOGIC)
   5.306 +    -m MODE      add print mode for output
   5.307 +    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
   5.308 +
   5.309 +  Run Isabelle process with plain tty interaction, and optional line editor.
   5.310 +\end{ttbox}
   5.311 +
   5.312 +  The \verb|-l| option specifies the logic image.  The
   5.313 +  \verb|-m| option specifies additional print modes.  The The
   5.314 +  \verb|-p| option specifies an alternative line editor (such
   5.315 +  as the \hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}} wrapper for GNU readline); the fall-back
   5.316 +  is to use raw standard input.%
   5.317 +\end{isamarkuptext}%
   5.318 +\isamarkuptrue%
   5.319 +%
   5.320 +\isamarkupsection{Remove awkward symbol names from theory sources%
   5.321 +}
   5.322 +\isamarkuptrue%
   5.323 +%
   5.324 +\begin{isamarkuptext}%
   5.325 +The \indexdef{}{tool}{unsymbolize}\hypertarget{tool.unsymbolize}{\hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}}} utility tunes Isabelle theory sources to
   5.326 +  improve readability for plain ASCII output (e.g.\ in email
   5.327 +  communication).  Most notably, \hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}} replaces awkward
   5.328 +  arrow symbols such as \verb|\|\verb|<Longrightarrow>|
   5.329 +  by \verb|==>|.
   5.330 +\begin{ttbox}
   5.331 +Usage: unsymbolize [FILES|DIRS...]
   5.332 +
   5.333 +  Recursively find .thy/.ML files, removing unreadable symbol names.
   5.334 +  Note: this is an ad-hoc script; there is no systematic way to replace
   5.335 +  symbols independently of the inner syntax of a theory!
   5.336 +
   5.337 +  Renames old versions of FILES by appending "~~".
   5.338 +\end{ttbox}%
   5.339 +\end{isamarkuptext}%
   5.340 +\isamarkuptrue%
   5.341 +%
   5.342 +\isamarkupsection{Output the version identifier of the Isabelle distribution%
   5.343 +}
   5.344 +\isamarkuptrue%
   5.345 +%
   5.346 +\begin{isamarkuptext}%
   5.347 +The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatt{version}}}}} utility outputs the full version string of
   5.348 +  the Isabelle distribution being used, e.g.\ ``\verb|Isabelle2008: June 2008|.  There are no options nor arguments.%
   5.349 +\end{isamarkuptext}%
   5.350 +\isamarkuptrue%
   5.351 +%
   5.352 +\isamarkupsection{Convert XML to YXML%
   5.353 +}
   5.354 +\isamarkuptrue%
   5.355 +%
   5.356 +\begin{isamarkuptext}%
   5.357 +The \indexdef{}{tool}{yxml}\hypertarget{tool.yxml}{\hyperlink{tool.yxml}{\mbox{\isa{\isatt{yxml}}}}} tool converts a standard XML document (stdin)
   5.358 +  to the much simpler and more efficient YXML format of Isabelle
   5.359 +  (stdout).  The YXML format is defined as follows.
   5.360 +
   5.361 +  \begin{enumerate}
   5.362 +
   5.363 +  \item The encoding is always UTF-8.
   5.364 +
   5.365 +  \item Body text is represented verbatim (no escaping, no special
   5.366 +  treatment of white space, no named entities, no CDATA chunks, no
   5.367 +  comments).
   5.368 +
   5.369 +  \item Markup elements are represented via ASCII control characters
   5.370 +  \isa{{\isachardoublequote}\isactrlbold X\ {\isacharequal}\ {\isadigit{5}}{\isachardoublequote}} and \isa{{\isachardoublequote}\isactrlbold Y\ {\isacharequal}\ {\isadigit{6}}{\isachardoublequote}} as follows:
   5.371 +
   5.372 +  \begin{tabular}{ll}
   5.373 +    XML & YXML \\\hline
   5.374 +    \verb|<|\isa{{\isachardoublequote}name\ attribute{\isachardoublequote}}\verb|=|\isa{{\isachardoublequote}value\ {\isasymdots}{\isachardoublequote}}\verb|>| &
   5.375 +    \isa{{\isachardoublequote}\isactrlbold X\isactrlbold Yname\isactrlbold Yattribute{\isachardoublequote}}\verb|=|\isa{{\isachardoublequote}value{\isasymdots}\isactrlbold X{\isachardoublequote}} \\
   5.376 +    \verb|</|\isa{name}\verb|>| & \isa{{\isachardoublequote}\isactrlbold X\isactrlbold Y\isactrlbold X{\isachardoublequote}} \\
   5.377 +  \end{tabular}
   5.378 +
   5.379 +  There is no special case for empty body text, i.e.\ \verb|<foo/>| is treated like \verb|<foo></foo>|.  Also note that
   5.380 +  \isa{{\isachardoublequote}\isactrlbold X{\isachardoublequote}} and \isa{{\isachardoublequote}\isactrlbold Y{\isachardoublequote}} may never occur in
   5.381 +  well-formed XML documents.
   5.382 +
   5.383 +  \end{enumerate}
   5.384 +
   5.385 +  Parsing YXML is pretty straight-forward: split the text into chunks
   5.386 +  separated by \isa{{\isachardoublequote}\isactrlbold X{\isachardoublequote}}, then split each chunk into
   5.387 +  sub-chunks separated by \isa{{\isachardoublequote}\isactrlbold Y{\isachardoublequote}}.  Markup chunks start
   5.388 +  with an empty sub-chunk, and a second empty sub-chunk indicates
   5.389 +  close of an element.  Any other non-empty chunk consists of plain
   5.390 +  text.
   5.391 +
   5.392 +  YXML documents may be detected quickly by checking that the first
   5.393 +  two characters are \isa{{\isachardoublequote}\isactrlbold X\isactrlbold Y{\isachardoublequote}}.%
   5.394 +\end{isamarkuptext}%
   5.395 +\isamarkuptrue%
   5.396 +%
   5.397 +\isadelimtheory
   5.398 +%
   5.399 +\endisadelimtheory
   5.400 +%
   5.401 +\isatagtheory
   5.402 +\isacommand{end}\isamarkupfalse%
   5.403 +%
   5.404 +\endisatagtheory
   5.405 +{\isafoldtheory}%
   5.406 +%
   5.407 +\isadelimtheory
   5.408 +%
   5.409 +\endisadelimtheory
   5.410 +\end{isabellebody}%
   5.411 +%%% Local Variables:
   5.412 +%%% mode: latex
   5.413 +%%% TeX-master: "root"
   5.414 +%%% End:
     6.1 --- a/doc-src/System/misc.tex	Mon Sep 15 19:43:10 2008 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,329 +0,0 @@
     6.4 -
     6.5 -% $Id$
     6.6 -
     6.7 -\chapter{Miscellaneous tools} \label{ch:tools}
     6.8 -
     6.9 -Subsequently we describe various Isabelle related utilities, given in
    6.10 -alphabetical order.
    6.11 -
    6.12 -
    6.13 -\section{Converting legacy ML scripts --- \texttt{isatool convert}}
    6.14 -
    6.15 -The \tooldx{convert} utility assists in converting legacy ML proof scripts
    6.16 -into the new-style format of Isabelle/Isar:
    6.17 -\begin{ttbox}
    6.18 -Usage: convert [FILES|DIRS...]
    6.19 -
    6.20 -  Recursively find .ML files, converting legacy tactic scripts to
    6.21 -  Isabelle/Isar tactic emulation.
    6.22 -  Note: conversion is only approximated, based on some heuristics.
    6.23 -
    6.24 -  Renames old versions of FILES by appending "~0~".
    6.25 -  Creates new versions of FILES by appending ".thy".
    6.26 -\end{ttbox}
    6.27 -The resulting theory text uses the tactic emulation facilities of
    6.28 -Isabelle/Isar (see also \cite{isabelle-ref}, especially the ``Conversion
    6.29 -guide'' in the appendix).  Usually there is some manual tuning required to get
    6.30 -an automatically converted script work again --- the success rate is around
    6.31 -99\% for common ML scripts.
    6.32 -
    6.33 -
    6.34 -\section{Displaying documents --- \texttt{isatool display}}
    6.35 -
    6.36 -The \tooldx{display} utility displays documents in DVI format:
    6.37 -\begin{ttbox}
    6.38 -Usage: display [OPTIONS] FILE
    6.39 -
    6.40 -  Options are:
    6.41 -    -c           cleanup -- remove FILE after use
    6.42 -
    6.43 -  Display document FILE (in DVI format).
    6.44 -\end{ttbox}
    6.45 -
    6.46 -\medskip The \texttt{-c} option causes the input file to be removed after use.
    6.47 -The program for viewing \texttt{dvi} files is determined by the
    6.48 -\texttt{DVI_VIEWER} setting.
    6.49 -
    6.50 -
    6.51 -\section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc}
    6.52 -
    6.53 -The \tooldx{doc} utility displays online documentation:
    6.54 -\begin{ttbox}
    6.55 -Usage: doc [DOC]
    6.56 -
    6.57 -  View Isabelle documentation DOC, or show list of available documents.
    6.58 -\end{ttbox}
    6.59 -If called without arguments, it lists all available documents. Each line
    6.60 -starts with an identifier, followed by a short description. Any of these
    6.61 -identifiers may be specified as the first argument in order to have the
    6.62 -corresponding document displayed.
    6.63 -
    6.64 -\medskip The \texttt{ISABELLE_DOCS} setting specifies the list of directories
    6.65 -(separated by colons) to be scanned for documentations.  The program for
    6.66 -viewing \texttt{dvi} files is determined by the \texttt{DVI_VIEWER} setting.
    6.67 -
    6.68 -
    6.69 -\section{Getting logic images --- \texttt{isatool findlogics}}
    6.70 -
    6.71 -The \tooldx{findlogics} utility traverses all directories specified in
    6.72 -\texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage is:
    6.73 -\begin{ttbox}
    6.74 -Usage: findlogics
    6.75 -
    6.76 -  Collect heap file names from ISABELLE_PATH.
    6.77 -\end{ttbox}
    6.78 -The base names of all files found on the path are printed --- sorted and with
    6.79 -duplicates removed. Also note that lookup in \texttt{ISABELLE_PATH} includes
    6.80 -the current values of \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}. Thus
    6.81 -switching to another {\ML} compiler may change the set of logic images
    6.82 -available.
    6.83 -
    6.84 -
    6.85 -\section{Inspecting the settings environment --- \texttt{isatool getenv}}
    6.86 -\label{sec:tool-getenv}
    6.87 -
    6.88 -The Isabelle settings environment --- as provided by the site-default and
    6.89 -user-specific settings files --- can be inspected with the \tooldx{getenv}
    6.90 -utility:
    6.91 -\begin{ttbox}
    6.92 -Usage: getenv [OPTIONS] [VARNAMES ...]
    6.93 -
    6.94 -  Options are:
    6.95 -    -a           display complete environment
    6.96 -    -b           print values only (doesn't work for -a)
    6.97 -
    6.98 -  Get value of VARNAMES from the Isabelle settings.
    6.99 -\end{ttbox}
   6.100 -
   6.101 -With the \texttt{-a} option, one may inspect the full process environment that
   6.102 -Isabelle related programs are run in. This usually contains much more
   6.103 -variables than are actually Isabelle settings.  Normally, output is a list of
   6.104 -lines of the form \mbox{$name$\texttt{=}$value$}. The \texttt{-b} option
   6.105 -causes only the values to be printed.
   6.106 -
   6.107 -
   6.108 -\subsection*{Examples}
   6.109 -
   6.110 -Get the {\ML} system name and the location where the compiler binaries are
   6.111 -supposed to reside as follows:
   6.112 -\begin{ttbox}
   6.113 -isatool getenv ML_SYSTEM ML_HOME
   6.114 -{\out ML_SYSTEM=polyml}
   6.115 -{\out ML_HOME=/usr/share/polyml/x86-linux}
   6.116 -\end{ttbox}
   6.117 -
   6.118 -The next one peeks at the output directory for \texttt{isabelle} logic images:
   6.119 -\begin{ttbox}
   6.120 -isatool getenv -b ISABELLE_OUTPUT
   6.121 -{\out /home/me/isabelle/heaps/polyml_x86-linux}
   6.122 -\end{ttbox}
   6.123 -Here we have used the \texttt{-b} option to suppress the
   6.124 -\texttt{ISABELLE_OUTPUT=} prefix.  The value above is what became of the
   6.125 -following assignment in the default settings file:
   6.126 -\begin{ttbox}
   6.127 -ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
   6.128 -\end{ttbox}
   6.129 -Note how the \texttt{ML_IDENTIFIER} value got appended automatically to each
   6.130 -path component. This is a special feature of \texttt{ISABELLE_OUTPUT}.
   6.131 -
   6.132 -
   6.133 -\section{Installing standalone Isabelle executables --- \texttt{isatool install}}
   6.134 -\label{sec:tool-install}
   6.135 -
   6.136 -By default, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool} etc.)
   6.137 -are just run from their location within the distribution directory, probably
   6.138 -indirectly by the shell through its \texttt{PATH}.  Other schemes of
   6.139 -installation are supported by the \tooldx{install} utility:
   6.140 -\begin{ttbox}
   6.141 -Usage: install [OPTIONS]
   6.142 -
   6.143 -  Options are:
   6.144 -    -d DISTDIR   use DISTDIR as Isabelle distribution
   6.145 -                 (default ISABELLE_HOME)
   6.146 -    -p DIR       install standalone binaries in DIR
   6.147 -
   6.148 -  Install Isabelle executables with absolute references to the current
   6.149 -  distribution directory.
   6.150 -\end{ttbox}
   6.151 -
   6.152 -The \texttt{-d} option overrides the current Isabelle distribution directory
   6.153 -as determined by \texttt{ISABELLE_HOME}.
   6.154 -
   6.155 -The \texttt{-p} option installs executable wrapper scripts for
   6.156 -\texttt{isabelle}, \texttt{isatool}, \texttt{Isabelle}, containing proper
   6.157 -absolute references to the Isabelle distribution directory.  A typical
   6.158 -\texttt{DIR} specification would be some directory expected to be in the
   6.159 -shell's \texttt{PATH}, such as \texttt{/usr/local/bin}.  It is important to
   6.160 -note that a plain manual copy of the original Isabelle executables just would
   6.161 -not work!
   6.162 -
   6.163 -
   6.164 -\section{Creating instances of the Isabelle logo --- \texttt{isatool
   6.165 -    logo}}
   6.166 -
   6.167 -The \tooldx{logo} utility creates any instance of the generic Isabelle logo as
   6.168 -an Encapsuled Postscript file (EPS):
   6.169 -\begin{ttbox}
   6.170 -Usage: logo [OPTIONS] NAME
   6.171 -
   6.172 -  Create instance NAME of the Isabelle logo (as EPS).
   6.173 -
   6.174 -  Options are:
   6.175 -    -o OUTFILE   set output file (default determined from NAME)
   6.176 -    -q           quiet mode
   6.177 -\end{ttbox}
   6.178 -You are encouraged to use this to create a derived logo for your Isabelle
   6.179 -project.  For example, \texttt{isatool logo Bali} creates
   6.180 -\texttt{isabelle_bali.eps}.
   6.181 -
   6.182 -
   6.183 -\section{Isabelle's version of make --- \texttt{isatool make}}
   6.184 -\label{sec:tool-make}
   6.185 -
   6.186 -The Isabelle \tooldx{make} utility is a very simple wrapper for
   6.187 -ordinary Unix \texttt{make}:
   6.188 -\begin{ttbox}
   6.189 -Usage: make [ARGS ...]
   6.190 -
   6.191 -  Compile the logic in current directory using IsaMakefile.
   6.192 -  ARGS are directly passed to the system make program.
   6.193 -\end{ttbox}
   6.194 -Note that the Isabelle settings environment is also active. Thus one
   6.195 -may refer to its values within the \ttindex{IsaMakefile}, e.g.\ 
   6.196 -\texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the
   6.197 -make file also inherit this environment.  Typically,
   6.198 -\texttt{IsaMakefile}s defer the real work to the \texttt{usedir}
   6.199 -utility, see \S\ref{sec:tool-usedir}.
   6.200 -
   6.201 -\medskip The basic \texttt{IsaMakefile} convention is that the default
   6.202 -target builds the actual logic, including its parents if appropriate.
   6.203 -The \texttt{images} target is intended to build all local logic
   6.204 -images, while the \texttt{test} target shall build all related
   6.205 -examples.  The \texttt{all} target shall do \texttt{images} and
   6.206 -\texttt{test}.
   6.207 -
   6.208 -
   6.209 -\subsection*{Examples}
   6.210 -
   6.211 -Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
   6.212 -object-logics as a model for your own developments.  For example, see
   6.213 -\texttt{src/FOL/IsaMakefile}.
   6.214 -
   6.215 -
   6.216 -\section{Make all logics --- \texttt{isatool makeall}}
   6.217 -
   6.218 -The \tooldx{makeall} utility applies Isabelle make to all logic
   6.219 -directories of the distribution:
   6.220 -\begin{ttbox}
   6.221 -Usage: makeall [ARGS ...]
   6.222 -
   6.223 -  Apply isatool make to all logics (passing ARGS).
   6.224 -\end{ttbox}
   6.225 -The arguments \texttt{ARGS} are just passed verbatim to each
   6.226 -\texttt{make} invocation.
   6.227 -
   6.228 -
   6.229 -\section{Printing documents --- \texttt{isatool print}}
   6.230 -
   6.231 -The \tooldx{print} utility prints documents:
   6.232 -\begin{ttbox}
   6.233 -Usage: print [OPTIONS] FILE
   6.234 -
   6.235 -  Options are:
   6.236 -    -c           cleanup -- remove FILE after use
   6.237 -
   6.238 -  Print document FILE.
   6.239 -\end{ttbox}
   6.240 -
   6.241 -The \texttt{-c} option causes the input file to be removed after use.  The
   6.242 -printer spool command is determined by the \texttt{PRINT_COMMAND} setting.
   6.243 -
   6.244 -
   6.245 -\section{Run Isabelle with plain tty interaction --- \texttt{isatool tty}} \label{sec:tool-tty}
   6.246 -
   6.247 -The \tooldx{tty} utility runs the Isabelle process interactively
   6.248 -within a plain terminal session:
   6.249 -\begin{ttbox}
   6.250 -Usage: tty [OPTIONS]
   6.251 -
   6.252 -  Options are:
   6.253 -    -l NAME      logic image name (default ISABELLE_LOGIC)
   6.254 -    -m MODE      add print mode for output
   6.255 -    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
   6.256 -
   6.257 -  Run Isabelle process with plain tty interaction, and optional line editor.
   6.258 -\end{ttbox}
   6.259 -
   6.260 -The \texttt{-l} option specifies the logic image.  The \texttt{-m}
   6.261 -option specifies additional print modes.  The The \texttt{-p} option
   6.262 -specifies an alternative line editor (such as the \texttt{rlwrap}
   6.263 -wrapper for GNU readline); the fall-back is to use raw standard input.
   6.264 -
   6.265 -
   6.266 -\section{Remove awkward symbol names from theory sources --- \texttt{isatool unsymbolize}}
   6.267 -
   6.268 -The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve
   6.269 -readability for plain ASCII output (e.g.\ in email communication).  Most
   6.270 -notably, \texttt{unsymbolize} replaces awkward arrow symbols such as
   6.271 -\verb|\<Longrightarrow>| by \verb|==>|.
   6.272 -\begin{ttbox}
   6.273 -Usage: unsymbolize [FILES|DIRS...]
   6.274 -
   6.275 -  Recursively find .thy/.ML files, removing unreadable symbol names.
   6.276 -  Note: this is an ad-hoc script; there is no systematic way to replace
   6.277 -  symbols independently of the inner syntax of a theory!
   6.278 -
   6.279 -  Renames old versions of FILES by appending "~~".
   6.280 -\end{ttbox}
   6.281 -
   6.282 -
   6.283 -\section{Output the version identifier of the Isabelle distribution --- \texttt{isatool version}}
   6.284 -
   6.285 -The \tooldx{version} utility outputs the full version string of the
   6.286 -Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007:
   6.287 -  November 2007}''.  There are no options nor arguments.
   6.288 -
   6.289 -
   6.290 -\section{Convert XML to YXML --- \texttt{isatool yxml}}
   6.291 -
   6.292 -The \tooldx{yxml} utility converts a standard XML document (stdin) to
   6.293 -the much simpler and more efficient YXML format of Isabelle (stdout).
   6.294 -The YXML format is defined as follows.
   6.295 -
   6.296 -\begin{enumerate}
   6.297 -
   6.298 -\item The encoding is always UTF-8.
   6.299 -
   6.300 -\item Body text is represented verbatim (no escaping, no special
   6.301 -  treatment of white space, no named entities, no CDATA chunks, no
   6.302 -  comments).
   6.303 -
   6.304 -\item Markup elements are represented via ASCII control characters $X
   6.305 -  = 5$ and $Y = 6$ as follows:
   6.306 -
   6.307 -  \begin{tabular}{ll}
   6.308 -    XML & YXML \\\hline
   6.309 -    \verb,<,\emph{name}~\emph{attribute}\verb,=,\emph{value}~\dots\verb,>, &
   6.310 -    \emph{X\,Y\,name\,Y\,attribute}\verb,=,\emph{value}\dots\emph{X} \\
   6.311 -    \verb,</,\emph{name}\verb,>, & \emph{X\,Y\,X} \\
   6.312 -  \end{tabular}
   6.313 -
   6.314 -  There is no special case for empty body text, i.e.\ \verb,<foo/>, is
   6.315 -  treated like \verb,<foo></foo>,.  Also note that \emph{X} and
   6.316 -  \emph{Y} may never occur in well-formed XML documents.
   6.317 -
   6.318 -\end{enumerate}
   6.319 -
   6.320 -Parsing YXML is pretty straight-forward: split the text into chunks separated
   6.321 -by \emph{X}, then split each chunk into sub-chunks separated by \emph{Y}.
   6.322 -Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
   6.323 -indicates close of an element.  Any other non-empty chunk consists of plain
   6.324 -text.
   6.325 -
   6.326 -YXML documents may be detected quickly by checking that the first two
   6.327 -characters are \emph{X\,Y}.
   6.328 -
   6.329 -%%% Local Variables: 
   6.330 -%%% mode: latex
   6.331 -%%% TeX-master: "system"
   6.332 -%%% End: 
     7.1 --- a/doc-src/System/system.tex	Mon Sep 15 19:43:10 2008 +0200
     7.2 +++ b/doc-src/System/system.tex	Mon Sep 15 20:22:38 2008 +0200
     7.3 @@ -38,7 +38,7 @@
     7.4  
     7.5  \input{Thy/document/Basics}
     7.6  \input{Thy/document/Presentation}
     7.7 -\input{misc}
     7.8 +\input{Thy/document/Misc}
     7.9  
    7.10  \appendix
    7.11  \let\int\intorig