document antiquotations are managed as theory data, with proper name space and entity markup;
%
\begin{isabellebody}%
\def\isabellecontext{Misc}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Misc\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Miscellaneous tools \label{ch:tools}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Subsequently we describe various Isabelle related utilities, given
in alphabetical order.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Displaying documents%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{display}\hypertarget{tool.display}{\hyperlink{tool.display}{\mbox{\isa{\isatt{display}}}}} utility displays documents in DVI or PDF
format:
\begin{ttbox}
Usage: display [OPTIONS] FILE
Options are:
-c cleanup -- remove FILE after use
Display document FILE (in DVI format).
\end{ttbox}
\medskip The \verb|-c| option causes the input file to be
removed after use. The program for viewing \verb|dvi| files is
determined by the \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Viewing documentation \label{sec:tool-doc}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{doc}\hypertarget{tool.doc}{\hyperlink{tool.doc}{\mbox{\isa{\isatt{doc}}}}} utility displays online documentation:
\begin{ttbox}
Usage: doc [DOC]
View Isabelle documentation DOC, or show list of available documents.
\end{ttbox}
If called without arguments, it lists all available documents. Each
line starts with an identifier, followed by a short description. Any
of these identifiers may be specified as the first argument in order
to have the corresponding document displayed.
\medskip The \hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCS}}}} setting specifies the list of
directories (separated by colons) to be scanned for documentations.
The program for viewing \verb|dvi| files is determined by the
\hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Getting logic images%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{findlogics}\hypertarget{tool.findlogics}{\hyperlink{tool.findlogics}{\mbox{\isa{\isatt{findlogics}}}}} utility traverses all directories
specified in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}}, looking for Isabelle logic
images. Its usage is:
\begin{ttbox}
Usage: findlogics
Collect heap file names from ISABELLE_PATH.
\end{ttbox}
The base names of all files found on the path are printed --- sorted
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}}}}
and \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}. Thus switching to another ML compiler
may change the set of logic images available.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Inspecting the settings environment \label{sec:tool-getenv}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The Isabelle settings environment --- as provided by the
site-default and user-specific settings files --- can be inspected
with the \indexdef{}{tool}{getenv}\hypertarget{tool.getenv}{\hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}} utility:
\begin{ttbox}
Usage: getenv [OPTIONS] [VARNAMES ...]
Options are:
-a display complete environment
-b print values only (doesn't work for -a)
-d FILE dump complete environment to FILE
(null terminated entries)
Get value of VARNAMES from the Isabelle settings.
\end{ttbox}
With the \verb|-a| option, one may inspect the full process
environment that Isabelle related programs are run in. This usually
contains much more variables than are actually Isabelle settings.
Normally, output is a list of lines of the form \isa{name}\verb|=|\isa{value}. The \verb|-b| option
causes only the values to be printed.
Option \verb|-d| produces a dump of the complete environment
to the specified file. Entries are terminated by the ASCII null
character, i.e.\ the C string terminator.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Get the ML system name and the location where the compiler binaries
are supposed to reside as follows:
\begin{ttbox}
isabelle getenv ML_SYSTEM ML_HOME
{\out ML_SYSTEM=polyml}
{\out ML_HOME=/usr/share/polyml/x86-linux}
\end{ttbox}
The next one peeks at the output directory for Isabelle logic
images:
\begin{ttbox}
isabelle getenv -b ISABELLE_OUTPUT
{\out /home/me/isabelle/heaps/polyml_x86-linux}
\end{ttbox}
Here we have used the \verb|-b| option to suppress the
\verb|ISABELLE_OUTPUT=| prefix. The value above is what
became of the following assignment in the default settings file:
\begin{ttbox}
ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
\end{ttbox}
Note how the \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}} value got appended
automatically to each path component. This is a special feature of
\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Installing standalone Isabelle executables \label{sec:tool-install}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}
etc.) are just run from their location within the distribution
directory, probably indirectly by the shell through its \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}. Other schemes of installation are supported by the
\indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
\begin{ttbox}
Usage: install [OPTIONS]
Options are:
-d DISTDIR use DISTDIR as Isabelle distribution
(default ISABELLE_HOME)
-p DIR install standalone binaries in DIR
Install Isabelle executables with absolute references to the current
distribution directory.
\end{ttbox}
The \verb|-d| option overrides the current Isabelle
distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}.
The \verb|-p| option installs executable wrapper scripts for
\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}},
\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the
Isabelle distribution directory. A typical \verb|DIR|
specification would be some directory expected to be in the shell's
\hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}, such as \verb|/usr/local/bin|. It is
important to note that a plain manual copy of the original Isabelle
executables does not work, since it disrupts the integrity of the
Isabelle distribution.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Creating instances of the Isabelle logo%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}} utility creates any instance of the generic
Isabelle logo as an Encapsuled Postscript file (EPS):
\begin{ttbox}
Usage: logo [OPTIONS] NAME
Create instance NAME of the Isabelle logo (as EPS).
Options are:
-o OUTFILE set output file (default determined from NAME)
-q quiet mode
\end{ttbox}
You are encouraged to use this to create a derived logo for your
Isabelle project. For example, \verb|isabelle| \hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}~\verb|Bali| creates \verb|isabelle_bali.eps|.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Isabelle's version of make \label{sec:tool-make}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The Isabelle \indexdef{}{tool}{make}\hypertarget{tool.make}{\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}} utility is a very simple wrapper for
ordinary Unix \hyperlink{executable.make}{\mbox{\isa{\isatt{make}}}}:
\begin{ttbox}
Usage: make [ARGS ...]
Compile the logic in current directory using IsaMakefile.
ARGS are directly passed to the system make program.
\end{ttbox}
Note that the Isabelle settings environment is also active. Thus one
may refer to its values within the \verb|IsaMakefile|, e.g.\
\verb|$(ISABELLE_OUTPUT)|. Furthermore, programs started from
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.
\medskip The basic \verb|IsaMakefile| convention is that the
default target builds the actual logic, including its parents if
appropriate. The \verb|images| target is intended to build all
local logic images, while the \verb|test| target shall build
all related examples. The \verb|all| target shall do
\verb|images| and \verb|test|.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
object-logics as a model for your own developments. For example,
see \verb|~~/src/FOL/IsaMakefile|.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Make all logics%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatt{makeall}}}}} utility applies Isabelle make to any
Isabelle component (cf.\ \secref{sec:components}) that contains an
\verb|IsaMakefile|:
\begin{ttbox}
Usage: makeall [ARGS ...]
Apply isabelle make to all components with IsaMakefile (passing ARGS).
\end{ttbox}
The arguments \verb|ARGS| are just passed verbatim to each
\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} invocation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Printing documents%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{print}\hypertarget{tool.print}{\hyperlink{tool.print}{\mbox{\isa{\isatt{print}}}}} utility prints documents:
\begin{ttbox}
Usage: print [OPTIONS] FILE
Options are:
-c cleanup -- remove FILE after use
Print document FILE.
\end{ttbox}
The \verb|-c| option causes the input file to be removed
after use. The printer spool command is determined by the \hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isaliteral{5F}{\isacharunderscore}}COMMAND}}}} setting.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Remove awkward symbol names from theory sources%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{unsymbolize}\hypertarget{tool.unsymbolize}{\hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}}} utility tunes Isabelle theory sources to
improve readability for plain ASCII output (e.g.\ in email
communication). Most notably, \hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}} replaces awkward
arrow symbols such as \verb|\|\verb|<Longrightarrow>|
by \verb|==>|.
\begin{ttbox}
Usage: unsymbolize [FILES|DIRS...]
Recursively find .thy/.ML files, removing unreadable symbol names.
Note: this is an ad-hoc script; there is no systematic way to replace
symbols independently of the inner syntax of a theory!
Renames old versions of FILES by appending "~~".
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Output the version identifier of the Isabelle distribution%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatt{version}}}}} utility displays Isabelle version information:
\begin{ttbox}
Usage: isabelle version [OPTIONS]
Options are:
-i short identification (derived from Mercurial id)
Display Isabelle version information.
\end{ttbox}
\medskip The default is to output the full version string of the
Isabelle distribution, e.g.\ ``\verb|Isabelle2011: January 2011|.
The \verb|-i| option produces a short identification derived
from the Mercurial id of the \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} directory.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Convert XML to YXML%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{yxml}\hypertarget{tool.yxml}{\hyperlink{tool.yxml}{\mbox{\isa{\isatt{yxml}}}}} tool converts a standard XML document (stdin)
to the much simpler and more efficient YXML format of Isabelle
(stdout). The YXML format is defined as follows.
\begin{enumerate}
\item The encoding is always UTF-8.
\item Body text is represented verbatim (no escaping, no special
treatment of white space, no named entities, no CDATA chunks, no
comments).
\item Markup elements are represented via ASCII control characters
\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:
\begin{tabular}{ll}
XML & YXML \\\hline
\verb|<|\isa{{\isaliteral{22}{\isachardoublequote}}name\ attribute{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}\verb|>| &
\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}}} \\
\verb|</|\isa{name}\verb|>| & \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} \\
\end{tabular}
There is no special case for empty body text, i.e.\ \verb|<foo/>| is treated like \verb|<foo></foo>|. Also note that
\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
well-formed XML documents.
\end{enumerate}
Parsing YXML is pretty straight-forward: split the text into chunks
separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}}, then split each chunk into
sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start
with an empty sub-chunk, and a second empty sub-chunk indicates
close of an element. Any other non-empty chunk consists of plain
text. For example, see \verb|~~/src/Pure/General/yxml.ML| or
\verb|~~/src/Pure/General/yxml.scala|.
YXML documents may be detected quickly by checking that the first
two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: