# HG changeset patch
# User wenzelm
# Date 1221500571 -7200
# Node ID 402a3f30542f7f8ec8e08b83bf9653e457b9bdac
# Parent  ca9fdab0f97106062657e20622e162fdfb3e84f3
generated files;

diff -r ca9fdab0f971 -r 402a3f30542f doc-src/System/Thy/document/Basics.tex
--- /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:
diff -r ca9fdab0f971 -r 402a3f30542f doc-src/System/Thy/document/Presentation.tex
--- /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: