--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/Thy/document/Basics.tex Mon Sep 15 19:42:51 2008 +0200
@@ -0,0 +1,561 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Basics}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Basics\isanewline
+\isakeyword{imports}\ Pure\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{The Isabelle system environment%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This manual describes Isabelle together with related tools and user
+ interfaces as seen from an outside (system oriented) view. See also
+ the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
+ and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
+ actual Isabelle commands and related functions.
+
+ \medskip The Isabelle system environment emerges from a few general
+ concepts.
+
+ \begin{itemize}
+
+ \item The \emph{Isabelle settings mechanism} provides environment
+ variables to all Isabelle programs (including tools and user
+ interfaces).
+
+ \item The \emph{Isabelle tools wrapper} (\indexdef{}{executable}{isatool}\hypertarget{executable.isatool}{\hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}}})
+ provides a generic startup platform for Isabelle related utilities.
+ Thus tools automatically benefit from the settings mechanism.
+
+ \item The raw \emph{Isabelle process} (\indexdef{}{executable}{isabelle}\hypertarget{executable.isabelle}{\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}} or
+ \indexdef{}{executable}{isabelle-process}\hypertarget{executable.isabelle-process}{\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}}) runs logic sessions either
+ interactively or in batch mode. In particular, this view abstracts
+ over the invocation of the actual ML system to be used.
+
+ \item The \emph{Isabelle interface wrapper} (\indexdef{}{executable}{Isabelle}\hypertarget{executable.Isabelle}{\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}} or \indexdef{}{executable}{isabelle-interface}\hypertarget{executable.isabelle-interface}{\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}}) provides some
+ abstraction over the actual user interface to be used. The de-facto
+ standard interface for Isabelle is Proof~General
+ \cite{proofgeneral}.
+
+ \end{itemize}
+
+ \medskip The beginning user would probably just run the default user
+ interface (by invoking the capital \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}). This
+ assumes that the system has already been installed, of course. In
+ case you have to do this yourself, see the \verb|INSTALL| file
+ in the top-level directory of the distribution of how to proceed;
+ binary packages for various system components are available as well.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Isabelle settings \label{sec:settings}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The Isabelle system heavily depends on the \emph{settings
+ mechanism}\indexbold{settings}. Essentially, this is a statically
+ scoped collection of environment variables, such as \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}, \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}, \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isacharunderscore}HOME}}}}. These
+ variables are \emph{not} intended to be set directly from the shell,
+ though. Isabelle employs a somewhat more sophisticated scheme of
+ \emph{settings files} --- one for site-wide defaults, another for
+ additional user-specific modifications. With all configuration
+ variables in at most two places, this scheme is more maintainable
+ and user-friendly than global shell environment variables.
+
+ In particular, we avoid the typical situation where prospective
+ users of a software package are told to put several things into
+ their shell startup scripts, before being able to actually run the
+ program. Isabelle requires none such administrative chores of its
+ end-users --- the executables can be invoked straight away.
+ Occasionally, users would still want to put the Isabelle \verb|bin| directory into their shell's search path, but this is not
+ required.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Building the environment%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Whenever any of the Isabelle executables is run, their settings
+ environment is put together as follows.
+
+ \begin{enumerate}
+
+ \item The special variable \indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}} is
+ determined automatically from the location of the binary that has
+ been run.
+
+ You should not try to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} manually. Also
+ note that the Isabelle executables either have to be run from their
+ original location in the distribution directory, or via the
+ executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility (see
+ \secref{sec:tool-install}). Just doing a plain copy of the
+ \verb|bin| files will not work!
+
+ \item The file \verb|$ISABELLE_HOME/etc/settings| ist run as
+ a shell script with the auto-export option for variables enabled.
+
+ This file holds a rather long list of shell variable assigments,
+ thus providing the site-wide default settings. The Isabelle
+ distribution already contains a global settings file with sensible
+ defaults for most variables. When installing the system, only a few
+ of these may have to be adapted (probably \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}
+ etc.).
+
+ \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
+ exists) is run in the same way as the site default settings. Note
+ that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set
+ before --- usually to \verb|~/isabelle|.
+
+ Thus individual users may override the site-wide defaults. See also
+ file \verb|etc/user-settings.sample| in the distribution.
+ Typically, a user settings file would contain only a few lines, just
+ the assigments that are really changed. One should definitely
+ \emph{not} start with a full copy the basic \verb|$ISABELLE_HOME/etc/settings|. This could cause very annoying
+ maintainance problems later, when the Isabelle installation is
+ updated or changed otherwise.
+
+ \end{enumerate}
+
+ Note that settings files are actually full GNU bash scripts. So one
+ may use complex shell commands, such as \verb|if| or
+ \verb|case| statements to set variables depending on the
+ system architecture or other environment variables. Such advanced
+ features should be added only with great care, though. In
+ particular, external environment references should be kept at a
+ minimum.
+
+ \medskip A few variables are somewhat special:
+
+ \begin{itemize}
+
+ \item \indexdef{}{setting}{ISABELLE}\hypertarget{setting.ISABELLE}{\hyperlink{setting.ISABELLE}{\mbox{\isa{\isatt{ISABELLE}}}}} and \indexdef{}{setting}{ISATOOL}\hypertarget{setting.ISATOOL}{\hyperlink{setting.ISATOOL}{\mbox{\isa{\isatt{ISATOOL}}}}} are set
+ automatically to the absolute path names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} executables,
+ respectively.
+
+ \item \indexdef{}{setting}{ISABELLE\_OUTPUT}\hypertarget{setting.ISABELLE-OUTPUT}{\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}} will have the identifiers of
+ the Isabelle distribution (cf.\ \hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}IDENTIFIER}}}}) and
+ the ML system (cf.\ \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}}) appended automatically
+ to its value.
+
+ \end{itemize}
+
+ \medskip The Isabelle settings scheme is conceptually simple, but
+ not completely trivial. For debugging purposes, the resulting
+ environment may be inspected with the \hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}} utility, see
+ \secref{sec:tool-getenv}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Common variables%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This is a reference of common Isabelle settings variables. Note that
+ the list is somewhat open-ended. Third-party utilities or interfaces
+ may add their own selection. Variables that are special in some
+ sense are marked with \isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}.
+
+ \begin{description}
+
+ \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is the
+ location of the top-level Isabelle distribution directory. This is
+ automatically determined from the Isabelle executable that has been
+ invoked. Do not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} yourself
+ from the shell.
+
+ \item[\indexdef{}{setting}{ISABELLE\_HOME\_USER}\hypertarget{setting.ISABELLE-HOME-USER}{\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}}}] is the user-specific
+ counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is
+ \verb|~/isabelle|, under rare circumstances this may be
+ changed in the global setting file. Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to
+ some extend. In particular, site-wide defaults may be overridden by
+ a private \verb|etc/settings|.
+
+ \item[\indexdef{}{setting}{ISABELLE}\hypertarget{setting.ISABELLE}{\hyperlink{setting.ISABELLE}{\mbox{\isa{\isatt{ISABELLE}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISATOOL}{\mbox{\isa{\isatt{ISATOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path
+ names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} executables, respectively. Thus other tools and scripts
+ need not assume that the Isabelle \verb|bin| directory is on
+ the current search path of the shell.
+
+ \item[\indexdef{}{setting}{ISABELLE\_IDENTIFIER}\hypertarget{setting.ISABELLE-IDENTIFIER}{\hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}IDENTIFIER}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] refers
+ to the name of this Isabelle distribution, e.g.\ ``\verb|Isabelle2008|''.
+
+ \item[\indexdef{}{setting}{ML\_SYSTEM}\hypertarget{setting.ML-SYSTEM}{\hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}}, \indexdef{}{setting}{ML\_HOME}\hypertarget{setting.ML-HOME}{\hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isacharunderscore}HOME}}}}},
+ \indexdef{}{setting}{ML\_OPTIONS}\hypertarget{setting.ML-OPTIONS}{\hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isacharunderscore}OPTIONS}}}}}, \indexdef{}{setting}{ML\_PLATFORM}\hypertarget{setting.ML-PLATFORM}{\hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}}}, \indexdef{}{setting}{ML\_IDENTIFIER}\hypertarget{setting.ML-IDENTIFIER}{\hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] specify the underlying ML system
+ to be used for Isabelle. There is only a fixed set of admissable
+ \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}} names (see the \verb|etc/settings| file
+ of the distribution).
+
+ The actual compiler binary will be run from the directory \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isacharunderscore}HOME}}}}, with \hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isacharunderscore}OPTIONS}}}} as first arguments on the
+ command line. The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}} may specify the
+ binary format of ML heap images, which is useful for cross-platform
+ installations. The value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is
+ automatically obtained by composing the values of \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}, \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}} and the Isabelle version values.
+
+ \item[\indexdef{}{setting}{ISABELLE\_PATH}\hypertarget{setting.ISABELLE-PATH}{\hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}}}] is a list of directories
+ (separated by colons) where Isabelle logic images may reside. When
+ looking up heaps files, the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is
+ appended to each component internally.
+
+ \item[\indexdef{}{setting}{ISABELLE\_OUTPUT}\hypertarget{setting.ISABELLE-OUTPUT}{\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is a
+ directory where output heap files should be stored by default. The
+ ML system and Isabelle version identifier is appended here, too.
+
+ \item[\indexdef{}{setting}{ISABELLE\_BROWSER\_INFO}\hypertarget{setting.ISABELLE-BROWSER-INFO}{\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}}] is the directory where
+ theory browser information (HTML text, graph data, and printable
+ documents) is stored (see also \secref{sec:info}). The default
+ value is \verb|$ISABELLE_HOME_USER/browser_info|.
+
+ \item[\indexdef{}{setting}{ISABELLE\_LOGIC}\hypertarget{setting.ISABELLE-LOGIC}{\hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}}}] specifies the default logic to
+ load if none is given explicitely by the user. The default value is
+ \verb|HOL|.
+
+ \item[\indexdef{}{setting}{ISABELLE\_LINE\_EDITOR}\hypertarget{setting.ISABELLE-LINE-EDITOR}{\hyperlink{setting.ISABELLE-LINE-EDITOR}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LINE{\isacharunderscore}EDITOR}}}}}] specifies the default
+ line editor for \verb|isatool tty| (see also
+ \secref{sec:tool-tty}).
+
+ \item[\indexdef{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hypertarget{setting.ISABELLE-USEDIR-OPTIONS}{\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed
+ to the command line of any \verb|isatool usedir| invocation
+ (see also \secref{sec:tool-usedir}). This typically contains
+ compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} is the
+ basic utility for managing logic sessions (cf.\ the \verb|IsaMakefile|s in the distribution).
+
+ \item[\indexdef{}{setting}{ISABELLE\_FILE\_IDENT}\hypertarget{setting.ISABELLE-FILE-IDENT}{\hyperlink{setting.ISABELLE-FILE-IDENT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}FILE{\isacharunderscore}IDENT}}}}}] specifies a shell command
+ for producing a source file identification, based on the actual
+ content instead of the full physical path and date stamp (which is
+ the default). A typical identification would produce a ``digest'' of
+ the text, using a cryptographic hash function like SHA-1, for
+ example.
+
+ \item[\indexdef{}{setting}{ISABELLE\_LATEX}\hypertarget{setting.ISABELLE-LATEX}{\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LATEX}}}}}, \indexdef{}{setting}{ISABELLE\_PDFLATEX}\hypertarget{setting.ISABELLE-PDFLATEX}{\hyperlink{setting.ISABELLE-PDFLATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PDFLATEX}}}}}, \indexdef{}{setting}{ISABELLE\_BIBTEX}\hypertarget{setting.ISABELLE-BIBTEX}{\hyperlink{setting.ISABELLE-BIBTEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BIBTEX}}}}}, \indexdef{}{setting}{ISABELLE\_DVIPS}\hypertarget{setting.ISABELLE-DVIPS}{\hyperlink{setting.ISABELLE-DVIPS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DVIPS}}}}}] refer to {\LaTeX} related tools for Isabelle
+ document preparation (see also \secref{sec:tool-latex}).
+
+ \item[\indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}}}] is a colon separated list of
+ directories that are scanned by \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} for external
+ utility programs (see also \secref{sec:isatool}).
+
+ \item[\indexdef{}{setting}{ISABELLE\_DOCS}\hypertarget{setting.ISABELLE-DOCS}{\hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DOCS}}}}}] is a colon separated list of
+ directories with documentation files.
+
+ \item[\indexdef{}{setting}{ISABELLE\_DOC\_FORMAT}\hypertarget{setting.ISABELLE-DOC-FORMAT}{\hyperlink{setting.ISABELLE-DOC-FORMAT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DOC{\isacharunderscore}FORMAT}}}}}] specifies the preferred
+ document format, typically \verb|dvi| or \verb|pdf|.
+
+ \item[\indexdef{}{setting}{DVI\_VIEWER}\hypertarget{setting.DVI-VIEWER}{\hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isacharunderscore}VIEWER}}}}}] specifies the command to be used
+ for displaying \verb|dvi| files.
+
+ \item[\indexdef{}{setting}{PDF\_VIEWER}\hypertarget{setting.PDF-VIEWER}{\hyperlink{setting.PDF-VIEWER}{\mbox{\isa{\isatt{PDF{\isacharunderscore}VIEWER}}}}}] specifies the command to be used
+ for displaying \verb|pdf| files.
+
+ \item[\indexdef{}{setting}{PRINT\_COMMAND}\hypertarget{setting.PRINT-COMMAND}{\hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isacharunderscore}COMMAND}}}}}] specifies the standard printer
+ spool command, which is expected to accept \verb|ps| files.
+
+ \item[\indexdef{}{setting}{ISABELLE\_TMP\_PREFIX}\hypertarget{setting.ISABELLE-TMP-PREFIX}{\hyperlink{setting.ISABELLE-TMP-PREFIX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TMP{\isacharunderscore}PREFIX}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is the
+ prefix from which any running \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} process derives
+ an individual directory for temporary files. The default is
+ somewhere in \verb|/tmp|.
+
+ \item[\indexdef{}{setting}{ISABELLE\_INTERFACE}\hypertarget{setting.ISABELLE-INTERFACE}{\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}}}] is an identifier that
+ specifies the actual user interface that the capital \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} or \hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}} should invoke. See
+ \secref{sec:interface} for more details.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{The Isabelle tools wrapper \label{sec:isatool}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+All Isabelle related utilities are called via a common wrapper ---
+ \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}}:
+
+\begin{ttbox}
+Usage: isatool TOOL [ARGS ...]
+
+ Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
+ for more specific help.
+
+ Available tools are:
+
+ browser - Isabelle graph browser
+ \dots
+\end{ttbox}
+
+ In principle, Isabelle tools are ordinary executable scripts that
+ are run within the Isabelle settings environment, see
+ \secref{sec:settings}. The set of available tools is collected by
+ \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} from the directories listed in the \hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}} setting. Do not try to call the scripts directly
+ from the shell. Neither should you add the tool directories to your
+ shell's search path!%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Show the list of available documentation of the current Isabelle
+ installation like this:
+
+\begin{ttbox}
+ isatool doc
+\end{ttbox}
+
+ View a certain document as follows:
+\begin{ttbox}
+ isatool doc isar-ref
+\end{ttbox}
+
+ Create an Isabelle session derived from HOL (see also
+ \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
+\begin{ttbox}
+ isatool mkdir HOL Test && isatool make
+\end{ttbox}
+ Note that \verb|isatool mkdir| is usually only invoked once;
+ existing sessions (including document output etc.) are then updated
+ by \verb|isatool make| alone.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{The raw Isabelle process%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} (or \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}) executable runs bare-bones Isabelle logic
+ sessions --- either interactively or in batch mode. It provides an
+ abstraction over the underlying ML system, and over the actual heap
+ file locations. Its usage is:
+
+\begin{ttbox}
+Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
+
+ Options are:
+ -C tell ML system to copy output image
+ -I startup Isar interaction mode
+ -P startup Proof General interaction mode
+ -S secure mode -- disallow critical operations
+ -W OUTPUT startup process wrapper, with messages going to OUTPUT stream
+ -X startup PGIP interaction mode
+ -c tell ML system to compress output image
+ -e MLTEXT pass MLTEXT to the ML session
+ -f pass 'Session.finish();' to the ML session
+ -m MODE add print mode for output
+ -q non-interactive session
+ -r open heap file read-only
+ -u pass 'use"ROOT.ML";' to the ML session
+ -w reset write permissions on OUTPUT
+
+ INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
+ These are either names to be searched in the Isabelle path, or
+ actual file names (containing at least one /).
+ If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
+\end{ttbox}
+
+ Input files without path specifications are looked up in the
+ \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}} setting, which may consist of multiple
+ components separated by colons --- these are tried in the given
+ order with the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} appended
+ internally. In a similar way, base names are relative to the
+ directory specified by \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}. In any case,
+ actual file locations may also be given by including at least one
+ slash (\verb|/|) in the name (hint: use \verb|./| to
+ refer to the current directory).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Options%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+If the input heap file does not have write permission bits set, or
+ the \verb|-r| option is given explicitely, then the session
+ started will be read-only. That is, the ML world cannot be
+ committed back into the image file. Otherwise, a writable session
+ enables commits into either the input file, or into another output
+ heap file (if that is given as the second argument on the command
+ line).
+
+ The read-write state of sessions is determined at startup only, it
+ cannot be changed intermediately. Also note that heap images may
+ require considerable amounts of disk space (approximately
+ 50--200~MB). Users are responsible for themselves to dispose their
+ heap files when they are no longer needed.
+
+ \medskip The \verb|-w| option makes the output heap file
+ read-only after terminating. Thus subsequent invocations cause the
+ logic image to be read-only automatically.
+
+ \medskip The \verb|-c| option tells the underlying ML system
+ to compress the output heap (fully transparently). On Poly/ML for
+ example, the image is garbage collected and all stored values are
+ maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
+ consumption.
+
+ \medskip The \verb|-C| option tells the ML system to produce
+ a completely self-contained output image, probably including a copy
+ of the ML runtime system itself.
+
+ \medskip Using the \verb|-e| option, arbitrary ML code may be
+ passed to the Isabelle session from the command line. Multiple
+ \verb|-e|'s are evaluated in the given order. Strange things
+ may happen when errorneous ML code is provided. Also make sure that
+ the ML commands are terminated properly by semicolon.
+
+ \medskip The \verb|-u| option is a shortcut for \verb|-e| passing ``\verb|use "ROOT.ML";|'' to the ML session.
+ The \verb|-f| option passes ``\verb|Session.finish();|'', which is intended mainly for administrative
+ purposes.
+
+ \medskip The \verb|-m| option adds identifiers of print modes
+ to be made active for this session. Typically, this is used by some
+ user interface, e.g.\ to enable output of proper mathematical
+ symbols.
+
+ \medskip Isabelle normally enters an interactive top-level loop
+ (after processing the \verb|-e| texts). The \verb|-q|
+ option inhibits interaction, thus providing a pure batch mode
+ facility.
+
+ \medskip The \verb|-I| option makes Isabelle enter Isar
+ interaction mode on startup, instead of the primitive ML top-level.
+ The \verb|-P| option configures the top-level loop for
+ interaction with the Proof General user interface, and the
+ \verb|-X| option enables XML-based PGIP communication. The
+ \verb|-W| option makes Isabelle enter a special process
+ wrapper for interaction via an external program; the protocol is a
+ stripped-down version of Proof General the interaction mode.
+
+ \medskip The \verb|-S| option makes the Isabelle process more
+ secure by disabling some critical operations, notably runtime
+ compilation and evaluation of ML source code.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Run an interactive session of the default object-logic (as specified
+ by the \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} setting) like this:
+\begin{ttbox}
+isabelle
+\end{ttbox}
+
+ Usually \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} refers to one of the standard
+ logic images, which are read-only by default. A writable session
+ --- based on \verb|FOL|, but output to \verb|Foo| (in the
+ directory specified by the \verb|ISABELLE_OUTPUT| setting) ---
+ may be invoked as follows:
+\begin{ttbox}
+isabelle FOL Foo
+\end{ttbox}
+ Ending this session normally (e.g.\ by typing control-D) dumps the
+ whole ML system state into \verb|Foo|. Be prepared for several
+ tens of megabytes.
+
+ The \verb|Foo| session may be continued later (still in
+ writable state) by:
+\begin{ttbox}
+isabelle Foo
+\end{ttbox}
+ A read-only \verb|Foo| session may be started by:
+\begin{ttbox}
+isabelle -r Foo
+\end{ttbox}
+
+ \medskip Note that manual session management like this does
+ \emph{not} provide proper setup for theory presentation. This would
+ require the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility, see \secref{sec:tool-usedir}.
+
+ \bigskip The next example demonstrates batch execution of
+ Isabelle. We print a certain theorem of \verb|FOL|:
+\begin{ttbox}
+isabelle -e "prth allE;" -q -r FOL
+\end{ttbox}
+ Note that the output text will be interspersed with additional junk
+ messages by the ML runtime environment.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{The Isabelle interface wrapper \label{sec:interface}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle is a generic theorem prover, even w.r.t.\ its user
+ interface. The \indexref{}{executable}{Isabelle}\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} (or \indexref{}{executable}{isabelle-interface}\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}) executable provides a uniform way for
+ end-users to invoke a certain interface; which one to start is
+ determined by the \indexref{}{setting}{ISABELLE\_INTERFACE}\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}} setting
+ variable, which should give a full path specification to the actual
+ executable. Also note that the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility provides
+ some options to install desktop environment icons (see
+ \secref{sec:tool-install}).
+
+ Presently, the most prominent Isabelle interface is Proof
+ General~\cite{proofgeneral}\index{user interface!Proof General}.
+ The Proof General distribution includes an interface wrapper script
+ for the regular Isar toplevel, see \verb|ProofGeneral/isar/interface|. The canonical settings for
+ Isabelle/Isar are as follows:
+
+\begin{ttbox}
+ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
+PROOFGENERAL_OPTIONS=""
+\end{ttbox}
+
+ Thus \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} would automatically invoke Emacs with
+ proper setup of the Proof General Lisp packages. There are some
+ options available, such as \verb|-l| for passing the logic
+ image to be used by default, or \verb|-m| to tune the
+ standard print mode. The \verb|-I| option allows to switch
+ between the Isar and ML view, independently of the interface script
+ being used.
+
+ \medskip Note that the world may be also seen the other way round:
+ Emacs may be started first (with proper setup of Proof General
+ mode), and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} run from within. This requires
+ further Emacs Lisp configuration, see the Proof General
+ documentation \cite{proofgeneral} for more information.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/Thy/document/Presentation.tex Mon Sep 15 19:42:51 2008 +0200
@@ -0,0 +1,794 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Presentation}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Presentation\isanewline
+\isakeyword{imports}\ Pure\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Presenting theories \label{ch:present}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle provides several ways to present the outcome of formal
+ developments, including WWW-based browsable libraries or actual
+ printable documents. Presentation is centered around the concept of
+ \emph{logic sessions}. The global session structure is that of a
+ tree, with Isabelle Pure at its root, further object-logics derived
+ (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
+ in leaf positions (usually without a separate image).
+
+ The Isabelle tools \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} and \indexref{}{tool}{make}\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} provide
+ the primary means for managing Isabelle sessions, including proper
+ setup for presentation. Here the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool takes care
+ to let \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} process run any
+ additional stages required for document preparation, notably the
+ tools \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} and \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}. The complete tool
+ chain for managing batch-mode Isabelle sessions is illustrated in
+ \figref{fig:session-tools}.
+
+ \begin{figure}[htbp]
+ \begin{center}
+ \begin{tabular}{lp{0.6\textwidth}}
+
+ \verb|isatool mkdir| & invoked once by the user to create
+ the initial source setup (common \verb|IsaMakefile| plus a
+ single session directory); \\
+
+ \verb|isatool make| & invoked repeatedly by the user to
+ keep session output up-to-date (HTML, documents etc.); \\
+
+ \verb|isatool usedir| & part of the standard \verb|IsaMakefile| entry of a session; \\
+
+ \verb|isabelle-process| & run through \verb|isatool|\isasep\isanewline%
+\verb| usedir|; \\
+
+ \verb|isatool document| & run by the Isabelle process if
+ document preparation is enabled; \\
+
+ \verb|isatool latex| & universal {\LaTeX} tool wrapper
+ invoked multiple times by \verb|isatool document|; also
+ useful for manual experiments; \\
+
+ \end{tabular}
+ \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
+ \end{center}
+ \end{figure}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Generating theory browser information \label{sec:info}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{theory browsing information|bold}
+
+ As a side-effect of running a logic sessions, Isabelle is able to
+ generate theory browsing information, including HTML documents that
+ show a theory's definition, the theorems proved in its ML file and
+ the relationship with its ancestors and descendants. Besides the
+ HTML file that is generated for every theory, Isabelle stores links
+ to all theories in an index file. These indexes are linked with
+ other indexes to represent the overall tree structure of logic
+ sessions.
+
+ Isabelle also generates graph files that represent the theory
+ hierarchy of a logic. There is a graph browser Java applet embedded
+ in the generated HTML pages, and also a stand-alone application that
+ allows browsing theory graphs without having to start a WWW client
+ first. The latter version also includes features such as generating
+ Postscript files, which are not available in the applet version.
+ See \secref{sec:browse} for further information.
+
+ \medskip
+
+ The easiest way to let Isabelle generate theory browsing information
+ for existing sessions is to append ``\verb|-i true|'' to the
+ \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} before invoking \verb|isatool make| (or \verb|./build| in the distribution). For
+ example, add something like this to your Isabelle settings file
+
+\begin{ttbox}
+ISABELLE_USEDIR_OPTIONS="-i true"
+\end{ttbox}
+
+ and then change into the \verb|src/FOL| directory of the
+ Isabelle distribution and run \verb|isatool make|, or even
+ \verb|isatool make all|. The presentation output will appear
+ in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
+ \verb|~/isabelle/browser_info/FOL|. Note that option
+ \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
+ more explicit about such details.
+
+ Many standard Isabelle sessions (such as \verb|HOL/ex|) also
+ provide actual printable documents. These are prepared
+ automatically as well if enabled like this, using the \verb|-d| option
+\begin{ttbox}
+ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
+\end{ttbox}
+ Enabling options \verb|-i| and \verb|-d|
+ simultaneausly as shown above causes an appropriate ``document''
+ link to be included in the HTML index. Documents (or raw document
+ sources) may be generated independently of browser information as
+ well, see \secref{sec:tool-document} for further details.
+
+ \bigskip The theory browsing information is stored in a
+ sub-directory directory determined by the \indexref{}{setting}{ISABELLE\_BROWSER\_INFO}\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} setting plus a prefix corresponding to the
+ session identifier (according to the tree structure of sub-sessions
+ by default). A complete WWW view of all standard object-logics and
+ examples of the Isabelle distribution is available at the Cambridge
+ or Munich Isabelle sites:
+ \begin{center}\small
+ \begin{tabular}{l}
+ \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
+ \url{http://isabelle.in.tum.de/library/} \\
+ \end{tabular}
+ \end{center}
+
+ \medskip In order to present your own theories on the web, simply
+ copy the corresponding subdirectory from \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} to your WWW server, having generated browser
+ info like this:
+\begin{ttbox}
+isatool usedir -i true HOL Foo
+\end{ttbox}
+
+ This assumes that directory \verb|Foo| contains some \verb|ROOT.ML| file to load all your theories, and HOL is your parent
+ logic image (\verb|isatool|~\indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} assists in
+ setting up Isabelle session directories. Theory browser information
+ for HOL should have been generated already beforehand.
+ Alternatively, one may specify an external link to an existing body
+ of HTML data by giving \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} a \verb|-P| option like
+ this:
+\begin{ttbox}
+isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
+\end{ttbox}
+
+ \medskip For production use, the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool is usually
+ invoked in an appropriate \verb|IsaMakefile|, via the Isabelle
+ \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} tool. There is a separate \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool to
+ provide easy setup of all this, with only minimal manual editing
+ required.
+\begin{ttbox}
+isatool mkdir HOL Foo && isatool make
+\end{ttbox}
+ See \secref{sec:tool-mkdir} for more information on preparing
+ Isabelle session directories, including the setup for documents.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Browsing theory graphs \label{sec:browse}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{theory graph browser|bold}
+
+ The Isabelle graph browser is a general tool for visualizing
+ dependency graphs. Certain nodes of the graph (i.e.~theories) can
+ be grouped together in ``directories'', whose contents may be
+ hidden, thus enabling the user to collapse irrelevant portions of
+ information. The browser is written in Java, it can be used both as
+ a stand-alone application and as an applet. Note that the option
+ \verb|-g| of \verb|isatool|~\indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
+ graph presentations in batch mode for inclusion in session
+ documents.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Invoking the graph browser%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The stand-alone version of the graph browser is wrapped up as an
+ Isabelle tool called \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatt{browser}}}}}:
+
+\begin{ttbox}
+Usage: browser [OPTIONS] [GRAPHFILE]
+
+ Options are:
+ -c cleanup -- remove GRAPHFILE after use
+ -o FILE output to FILE (ps, eps, pdf)
+\end{ttbox}
+ When no filename is specified, the browser automatically changes to
+ the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}.
+
+ \medskip The \verb|-c| option causes the input file to be
+ removed after use.
+
+ The \verb|-o| option indicates batch-mode operation, with the
+ output written to the indicated file; note that \verb|pdf|
+ produces an \verb|eps| copy as well.
+
+ \medskip The applet version of the browser is part of the standard
+ WWW theory presentation, see the link ``theory dependencies'' within
+ each session index.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Using the graph browser%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The browser's main window, which is shown in
+ \figref{fig:browserwindow}, consists of two sub-windows. In the
+ left sub-window, the directory tree is displayed. The graph itself
+ is displayed in the right sub-window.
+
+ \begin{figure}[ht]
+ \includegraphics[width=\textwidth]{browser_screenshot}
+ \caption{\label{fig:browserwindow} Browser main window}
+ \end{figure}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The directory tree window%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We describe the usage of the directory browser and the meaning of
+ the different items in the browser window.
+
+ \begin{itemize}
+
+ \item A red arrow before a directory name indicates that the
+ directory is currently ``folded'', i.e.~the nodes in this directory
+ are collapsed to one single node. In the right sub-window, the names
+ of nodes corresponding to folded directories are enclosed in square
+ brackets and displayed in red color.
+
+ \item A green downward arrow before a directory name indicates that
+ the directory is currently ``unfolded''. It can be folded by
+ clicking on the directory name. Clicking on the name for a second
+ time unfolds the directory again. Alternatively, a directory can
+ also be unfolded by clicking on the corresponding node in the right
+ sub-window.
+
+ \item Blue arrows stand before ordinary node names. When clicking on
+ such a name (i.e.\ that of a theory), the graph display window
+ focuses to the corresponding node. Double clicking invokes a text
+ viewer window in which the contents of the theory file are
+ displayed.
+
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The graph display window%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+When pointing on an ordinary node, an upward and a downward arrow is
+ shown. Initially, both of these arrows are green. Clicking on the
+ upward or downward arrow collapses all predecessor or successor
+ nodes, respectively. The arrow's color then changes to red,
+ indicating that the predecessor or successor nodes are currently
+ collapsed. The node corresponding to the collapsed nodes has the
+ name ``\verb|[....]|''. To uncollapse the nodes again, simply
+ click on the red arrow or on the node with the name ``\verb|[....]|''. Similar to the directory browser, the contents of
+ theory files can be displayed by double clicking on the
+ corresponding node.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The ``File'' menu%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Due to Java Applet security restrictions this menu is only available
+ in the full application version. The meaning of the menu items is as
+ follows:
+
+ \begin{description}
+
+ \item[Open \dots] Open a new graph file.
+
+ \item[Export to PostScript] Outputs the current graph in Postscript
+ format, appropriately scaled to fit on one single sheet of A4 paper.
+ The resulting file can be printed directly.
+
+ \item[Export to EPS] Outputs the current graph in Encapsulated
+ Postscript format. The resulting file can be included in other
+ documents.
+
+ \item[Quit] Quit the graph browser.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Syntax of graph definition files%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A graph definition file has the following syntax:
+
+ \begin{tabular}{rcl}
+ \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
+ \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}\isactrlsup {\isacharasterisk}{\isachardoublequote}}
+ \end{tabular}
+
+ The meaning of the items in a vertex description is as follows:
+
+ \begin{description}
+
+ \item[\isa{vertex{\isacharunderscore}name}] The name of the vertex.
+
+ \item[\isa{vertex{\isacharunderscore}ID}] The vertex identifier. Note that there may
+ be several vertices with equal names, whereas identifiers must be
+ unique.
+
+ \item[\isa{dir{\isacharunderscore}name}] The name of the ``directory'' the vertex
+ should be placed in. A ``\verb|+|'' sign after \isa{dir{\isacharunderscore}name} indicates that the nodes in the directory are initially
+ visible. Directories are initially invisible by default.
+
+ \item[\isa{path}] The path of the corresponding theory file. This
+ is specified relatively to the path of the graph definition file.
+
+ \item[List of successor/predecessor nodes] A ``\verb|<|''
+ sign before the list means that successor nodes are listed, a
+ ``\verb|>|'' sign means that predecessor nodes are listed. If
+ neither ``\verb|<|'' nor ``\verb|>|'' is found, the
+ browser assumes that successor nodes are listed.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Creating Isabelle session directories
+ \label{sec:tool-mkdir}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{mkdir}\hypertarget{tool.mkdir}{\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}} utility prepares Isabelle session source
+ directories, including a sensible default setup of \verb|IsaMakefile|, \verb|ROOT.ML|, and a \verb|document|
+ directory with a minimal \verb|root.tex| that is sufficient to
+ print all theories of the session (in the order of appearance); see
+ \secref{sec:tool-document} for further information on Isabelle
+ document preparation. The usage of \verb|isatool mkdir| is:
+
+\begin{ttbox}
+Usage: mkdir [OPTIONS] [LOGIC] NAME
+
+ Options are:
+ -I FILE alternative IsaMakefile output
+ -P include parent logic target
+ -b setup build mode (session outputs heap image)
+ -q quiet mode
+
+ Prepare session directory, including IsaMakefile and document source,
+ with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
+\end{ttbox}
+
+ The \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool is conservative in the sense that any
+ existing \verb|IsaMakefile| etc.\ is left unchanged. Thus it
+ is safe to invoke it multiple times, although later runs may not
+ have the desired effect.
+
+ Note that \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is unable to change \verb|IsaMakefile|
+ incrementally --- manual changes are required for multiple
+ sub-sessions. On order to get an initial working session, the only
+ editing needed is to add appropriate \verb|use_thy| calls to the
+ generated \verb|ROOT.ML| file.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Options%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \verb|-I| option specifies an alternative to \verb|IsaMakefile| for dependencies. Note that ``\verb|-|'' refers
+ to \emph{stdout}, i.e.\ ``\verb|-I-|'' provides an easy way
+ to peek at \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}'s idea of \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} setup required for
+ some particular of Isabelle session.
+
+ \medskip The \verb|-P| option includes a target for the
+ parent \verb|LOGIC| session in the generated \verb|IsaMakefile|. The corresponding sources are assumed to be located
+ within the Isabelle distribution.
+
+ \medskip The \verb|-b| option sets up the current directory
+ as the base for a new session that provides an actual logic image,
+ as opposed to one that only runs several theories based on an
+ existing image. Note that in the latter case, everything except
+ \verb|IsaMakefile| would be placed into a separate directory
+ \verb|NAME|, rather than the current one. See
+ \secref{sec:tool-usedir} for further information on \emph{build
+ mode} vs.\ \emph{example mode} of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
+
+ \medskip The \verb|-q| option enables quiet mode, suppressing
+ further notes on how to proceed.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The standard setup of a single ``example session'' based on the
+ default logic, with proper document generation is generated like
+ this:
+\begin{ttbox}
+isatool mkdir Foo && isatool make
+\end{ttbox}
+
+ \noindent The theory sources should be put into the \verb|Foo|
+ directory, and its \verb|ROOT.ML| should be edited to load all
+ required theories. Invoking \verb|isatool make| again would
+ run the whole session, generating browser information and the
+ document automatically. The \verb|IsaMakefile| is typically
+ tuned manually later, e.g.\ adding source dependencies, or changing
+ the options passed to \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}.
+
+ \medskip Large projects may demand further sessions, potentially
+ with separate logic images being created. This usually requires
+ manual editing of the generated \verb|IsaMakefile|, which is
+ meant to cover all of the sub-session directories at the same time
+ (this is the deeper reasong why \verb|IsaMakefile| is not made
+ part of the initial session directory created by \verb|isatool|\isasep\isanewline%
+\verb| mkdir|). See \verb|src/HOL/IsaMakefile| of the Isabelle
+ distribution for a full-blown example.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Running Isabelle sessions \label{sec:tool-usedir}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{usedir}\hypertarget{tool.usedir}{\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}} utility builds object-logic images, or runs
+ example sessions based on existing logics. Its usage is:
+\begin{ttbox}
+
+Usage: usedir [OPTIONS] LOGIC NAME
+
+ Options are:
+ -C BOOL copy existing document directory to -D PATH (default true)
+ -D PATH dump generated document sources into PATH
+ -M MAX multithreading: maximum number of worker threads (default 1)
+ -P PATH set path for remote theory browsing information
+ -T LEVEL multithreading: trace level (default 0)
+ -V VERSION declare alternative document VERSION
+ -b build mode (output heap image, using current dir)
+ -c BOOL tell ML system to compress output image (default true)
+ -d FORMAT build document as FORMAT (default false)
+ -f NAME use ML file NAME (default ROOT.ML)
+ -g BOOL generate session graph image for document (default false)
+ -i BOOL generate theory browser information (default false)
+ -m MODE add print mode for output
+ -p LEVEL set level of detail for proof objects
+ -r reset session path
+ -s NAME override session NAME
+ -v BOOL be verbose (default false)
+
+ Build object-logic or run examples. Also creates browsing
+ information (HTML etc.) according to settings.
+
+ ISABELLE_USEDIR_OPTIONS=
+ HOL_USEDIR_OPTIONS=
+\end{ttbox}
+
+ Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}
+ setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
+ call. Since the \verb|IsaMakefile|s of all object-logics
+ distributed with Isabelle just invoke \texttt{usedir} for the real
+ work, one may control compilation options globally via above
+ variable. In particular, generation of \rmindex{HTML} browsing
+ information and document preparation is controlled here.
+
+ The \indexref{}{setting}{HOL\_USEDIR\_OPTIONS}\hyperlink{setting.HOL-USEDIR-OPTIONS}{\mbox{\isa{\isatt{HOL{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} setting is specific to the
+ plain and main Isabelle/HOL images; its value is appended to
+ \hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} for these particular sessions
+ only.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Options%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Basically, there are two different modes of operation: \emph{build
+ mode} (enabled through the \verb|-b| option) and
+ \emph{example mode} (default).
+
+ Calling \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} with \verb|-b| runs \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} with input image \verb|LOGIC| and output to
+ \verb|NAME|, as provided on the command line. This will be a
+ batch session, running \verb|ROOT.ML| from the current
+ directory and then quitting. It is assumed that \verb|ROOT.ML|
+ contains all ML commands required to build the logic.
+
+ In example mode, \verb|usedir| runs a read-only session of
+ \verb|LOGIC| and automatically runs \verb|ROOT.ML| from
+ within directory \verb|NAME|. It assumes that this file
+ contains appropriate ML commands to run the desired examples.
+
+ \medskip The \verb|-i| option controls theory browser data
+ generation. It may be explicitly turned on or off --- as usual, the
+ last occurrence of \verb|-i| on the command line wins.
+
+ The \verb|-P| option specifies a path (or actual URL) to be
+ prefixed to any \emph{non-local} reference of existing theories.
+ Thus user sessions may easily link to existing Isabelle libraries
+ already present on the WWW.
+
+ The \verb|-m| options specifies additional print modes to be
+ activated temporarily while the session is processed.
+
+ \medskip The \verb|-d| option controls document preparation.
+ Valid arguments are \verb|false| (do not prepare any document;
+ this is default), or any of \verb|dvi|, \verb|dvi.gz|,
+ \verb|ps|, \verb|ps.gz|, \verb|pdf|. The logic
+ session has to provide a properly setup \verb|document|
+ directory. See \secref{sec:tool-document} and
+ \secref{sec:tool-latex} for more details.
+
+ \medskip The \verb|-V| option declares alternative document
+ versions, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool). The
+ standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
+ commands, proof body texts, and ML code will be presented
+ faithfully. An alternative version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
+ original text by a short place-holder. The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
+ the list of versions to be processed. Any number of \verb|-V| options may be given; later declarations have precedence over
+ earlier ones.
+
+ \medskip The \verb|-g| option produces images of the theory
+ dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
+ generated document, both as \verb|session_graph.eps| and
+ \verb|session_graph.pdf| at the same time. To include this in
+ the final {\LaTeX} document one could say \verb|\includegraphics{session_graph}| in \verb|document/root.tex| (omitting the file-name extension enables
+ {\LaTeX} to select to correct version, either for the DVI or PDF
+ output path).
+
+ \medskip The \verb|-D| option causes the generated document
+ sources to be dumped at location \verb|PATH|; this path is
+ relative to the session's main directory. If the \verb|-C|
+ option is true, this will include a copy of an existing \verb|document| directory as provided by the user. For example,
+ \verb|isatool usedir -D generated HOL Foo| produces a
+ complete set of document sources at \verb|Foo/generated|.
+ Subsequent invocation of \verb|isatool document|\isasep\isanewline%
+\verb| Foo/generated| (see also \secref{sec:tool-document}) will process
+ the final result independently of an Isabelle job. This decoupled
+ mode of operation facilitates debugging of serious {\LaTeX} errors,
+ for example.
+
+ \medskip The \verb|-p| option determines the level of detail
+ for internal proof objects, see also the \emph{Isabelle Reference
+ Manual}~\cite{isabelle-ref}.
+
+ \medskip The \verb|-v| option causes additional information
+ to be printed while running the session, notably the location of
+ prepared documents.
+
+ \medskip The \verb|-M| option specifies the maximum number of
+ parallel threads used for processing independent tasks when checking
+ theory sources (multithreading only works on suitable ML platforms).
+ The special value of ``\verb|0|'' or ``\verb|max|'' refers
+ to the number of actual CPU cores of the underlying machine, which
+ is a good starting point for optimal performance tuning. The
+ \verb|-T| option determines the level of detail in tracing
+ output concerning the internal locking and scheduling in
+ multithreaded operation. This may be helpful in isolating
+ performance bottle-necks, e.g.\ due to excessive wait states when
+ locking critical code sections.
+
+ \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
+ identifier}. These accumulate, documenting the way sessions depend
+ on others. For example, consider \verb|Pure/FOL/ex|, which
+ refers to the examples of FOL, which in turn is built upon Pure.
+
+ The current session's identifier is by default just the base name of
+ the \verb|LOGIC| argument (in build mode), or of the \verb|NAME| argument (in example mode). This may be overridden explicitly
+ via the \verb|-s| option.%
+\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|. The Isabelle \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
+ of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Preparing Isabelle session documents
+ \label{sec:tool-document}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{document}\hypertarget{tool.document}{\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}} utility prepares logic session documents,
+ processing the sources both as provided by the user and generated by
+ Isabelle. Its usage is:
+\begin{ttbox}
+Usage: document [OPTIONS] [DIR]
+
+ Options are:
+ -c cleanup -- be aggressive in removing old stuff
+ -n NAME specify document name (default 'document')
+ -o FORMAT specify output format: dvi (default), dvi.gz, ps,
+ ps.gz, pdf
+ -t TAGS specify tagged region markup
+
+ Prepare the theory session document in DIR (default 'document')
+ producing the specified output format.
+\end{ttbox}
+ This tool is usually run automatically as part of the corresponding
+ Isabelle batch process, provided document preparation has been
+ enabled (cf.\ the \verb|-d| option of the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
+ tool). It may be manually invoked on the generated browser
+ information document output as well, e.g.\ in case of errors
+ encountered in the batch run.
+
+ \medskip The \verb|-c| option tells the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool
+ to dispose the document sources after successful operation. This is
+ the right thing to do for sources generated by an Isabelle process,
+ but take care of your files in manual document preparation!
+
+ \medskip The \verb|-n| and \verb|-o| option specify
+ the final output file name and format, the default is ``\verb|document.dvi|''. Note that the result will appear in the parent of
+ the target \verb|DIR|.
+
+ \medskip The \verb|-t| option tells {\LaTeX} how to interpret
+ tagged Isabelle command regions. Tags are specified as a comma
+ separated list of modifier/name pairs: ``\verb|+|\isa{foo}'' (or just ``\isa{foo}'') means to keep, ``\verb|-|\isa{foo}'' to drop, and ``\verb|/|\isa{foo}'' to
+ fold text tagged as \isa{foo}. The builtin default is equivalent
+ to the tag specification ``\verb|/theory,/proof,/ML,+visible,-invisible|''; see also the {\LaTeX}
+ macros \verb|\isakeeptag|, \verb|\isadroptag|, and
+ \verb|\isafoldtag|, in \verb|isabelle.sty|.
+
+ \medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources. This
+ directory is supposed to contain all the files needed to produce the
+ final document --- apart from the actual theories which are
+ generated by Isabelle.
+
+ \medskip For most practical purposes, the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool is
+ smart enough to create any of the specified output formats, taking
+ \verb|root.tex| supplied by the user as a starting point. This
+ even includes multiple runs of {\LaTeX} to accommodate references
+ and bibliographies (the latter assumes \verb|root.bib| within
+ the same directory).
+
+ In more complex situations, a separate \verb|IsaMakefile| for
+ the document sources may be given instead. This should provide
+ targets for any admissible document format; these have to produce
+ corresponding output files named after \verb|root| as well,
+ e.g.\ \verb|root.dvi| for target format \verb|dvi|.
+
+ \medskip When running the session, Isabelle copies the original
+ \verb|document| directory into its proper place within
+ \verb|ISABELLE_BROWSER_INFO| according to the session path.
+ Then, for any processed theory \isa{A} some {\LaTeX} source is
+ generated and put there as \isa{A}\verb|.tex|.
+ Furthermore, a list of all generated theory files is put into
+ \verb|session.tex|. Typically, the root {\LaTeX} file provided
+ by the user would include \verb|session.tex| to get a document
+ containing all the theories.
+
+ The {\LaTeX} versions of the theories require some macros defined in
+ \verb|isabelle.sty| as distributed with Isabelle. Doing
+ \verb|\usepackage{isabelle}| in \verb|root.tex| should
+ be fine; the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes
+ an appropriate path specification for {\TeX} inputs.
+
+ If the text contains any references to Isabelle symbols (such as
+ \verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well. This package contains
+ a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, (see \appref{app:symbols} for a
+ complete list of predefined Isabelle symbols). Users may invent
+ further symbols as well, just by providing {\LaTeX} macros in a
+ similar fashion as in \verb|isabellesym.sty| of the
+ distribution.
+
+ For proper setup of DVI and PDF documents (with hyperlinks and
+ bookmarks), we recommend to include \verb|pdfsetup.sty| as
+ well.
+
+ \medskip As a final step of document preparation within Isabelle,
+ \verb|isatool document -c| is run on the resulting \verb|document| directory. Thus the actual output document is built and
+ installed in its proper place (as linked by the session's \verb|index.html| if option \verb|-i| of \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} has
+ been enabled, cf.\ \secref{sec:info}). The generated sources are
+ deleted after successful run of {\LaTeX} and friends. Note that a
+ separate copy of the sources may be retained by passing an option
+ \verb|-D| to the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility when running the
+ session.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Running {\LaTeX} within the Isabelle environment
+ \label{sec:tool-latex}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{latex}\hypertarget{tool.latex}{\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}} utility provides the basic interface for
+ Isabelle document preparation. Its usage is:
+\begin{ttbox}
+Usage: latex [OPTIONS] [FILE]
+
+ Options are:
+ -o FORMAT specify output format: dvi (default), dvi.gz, ps,
+ ps.gz, pdf, bbl, idx, sty, syms
+
+ Run LaTeX (and related tools) on FILE (default root.tex),
+ producing the specified output format.
+\end{ttbox}
+
+ Appropriate {\LaTeX}-related programs are run on the input file,
+ according to the given output format: \hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}},
+ \hyperlink{executable.pdflatex}{\mbox{\isa{\isatt{pdflatex}}}}, \hyperlink{executable.dvips}{\mbox{\isa{\isatt{dvips}}}}, \hyperlink{executable.bibtex}{\mbox{\isa{\isatt{bibtex}}}}
+ (for \verb|bbl|), and \hyperlink{executable.makeindex}{\mbox{\isa{\isatt{makeindex}}}} (for \verb|idx|). The actual commands are determined from the settings
+ environment (\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LATEX}}}} etc.).
+
+ The \verb|sty| output format causes the Isabelle style files to
+ be updated from the distribution. This is useful in special
+ situations where the document sources are to be processed another
+ time by separate tools (cf.\ option \verb|-D| of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility).
+
+ The \verb|syms| output is for internal use; it generates lists
+ of symbols that are available without loading additional {\LaTeX}
+ packages.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Invoking \verb|isatool latex| by hand may be occasionally
+ useful when debugging failed attempts of the automatic document
+ preparation stage of batch-mode Isabelle. The abortive process
+ leaves the sources at a certain place within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}, see the runtime error message for details.
+ This enables users to inspect {\LaTeX} runs in further detail, e.g.\
+ like this:
+\begin{ttbox}
+ cd ~/isabelle/browser_info/HOL/Test/document
+ isatool latex -o pdf
+\end{ttbox}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: