--- a/doc-src/System/basics.tex Wed Oct 13 15:41:24 1999 +0200
+++ b/doc-src/System/basics.tex Wed Oct 13 19:39:19 1999 +0200
@@ -3,21 +3,21 @@
\chapter{Basic concepts}
-The \emph{Isabelle System Manual} describes Isabelle together with
-related tools and user interfaces as seen from an outside (operating
-system oriented) view. See the \emph{Isabelle Reference Manual} for
-all internal {\ML} level user commands, on the other hand.
+The \emph{Isabelle System Manual} describes Isabelle together with related
+tools and user interfaces as seen from an outside, operating system oriented
+view. See the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} and the
+\emph{Isabelle Isar Reference Manual}~\cite{isabelle-isar-ref} for the
+internal user commands, on the other hand.
-\medskip The Isabelle system level environment is based on a few
-general concepts:
+\medskip The Isabelle system environment is based on a few general elements:
\begin{itemize}
\item The \emph{Isabelle settings mechanism}, which provides
environment variables to all Isabelle programs (including tools and
user interfaces).
-\item \emph{Isabelle proper} (\ttindex{isabelle}), which runs logic
+\item \emph{Isabelle proper} (\ttindex{isabelle}), which invokes logic
sessions, both interactively or in batch mode. In particular,
- \texttt{isabelle} abstracts over the invocation of the actual {\ML}
- system to be used.
+ \texttt{isabelle} abstracts over the invocation of the actual {\ML} system
+ to be used.
\item The \emph{Isabelle tools wrapper} (\ttindex{isatool}), which
provides a generic startup platform for Isabelle related utilities.
Thus tools automatically benefit from the settings mechanism.
@@ -84,11 +84,11 @@
sensible defaults for most variables. When installing the system,
only a few of these have to be adapted (most likely
\texttt{ML_SYSTEM} etc.).
-
-\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it
- exists) is run the same way as the site default settings. The
- variable \texttt{ISABELLE_HOME_USER} has already been set before ---
- usually to \texttt{\~\relax/isabelle}.
+
+\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is
+ run the same way as the site default settings. Note that the variable
+ \texttt{ISABELLE_HOME_USER} has already been set before --- usually to
+ \texttt{\~\relax/isabelle}.
Thus individual users may override the site-wide defaults. See also
file \texttt{etc/user-settings.sample} in the distribution.
@@ -186,6 +186,10 @@
options for object-logics --- \texttt{usedir} is the basic utility
that builds them (cf.\ the \texttt{IsaMakefile}s in the
distribution).
+
+\item[\settdx{ISABELLE_LATEX}, \settdx{ISABELLE_PDFLATEX},
+ \settdx{ISABELLE_BIBTEX}, \settdx{ISABELLE_DVIPS}] refer to {\LaTeX} related
+ tools for Isabelle document preparation (see also \S\ref{sec:tool-latex}).
\item[\settdx{ISABELLE_TOOLS}] is a colon separated list of
directories that are scanned by \texttt{isatool} for utility
@@ -238,12 +242,12 @@
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
-\texttt{ISABELLE_PATH} setting, which may consist of multiple
-components separated by colons --- these are tried in order.
-Likewise, base names are relative to the directory specified by
-\texttt{ISABELLE_OUTPUT}. In any case, actual file locations may also
-be given by including at least one \texttt{/} in the name (hint: use
-\texttt{./} to refer to the current directory).
+\texttt{ISABELLE_PATH} setting, which may consist of multiple components
+separated by colons --- these are tried in order. Likewise, base names are
+relative to the directory specified by \texttt{ISABELLE_OUTPUT}. In any case,
+actual file locations may also be given by including at least one slash
+(\texttt{/}) in the name (hint: use \texttt{./} to refer to the current
+directory).
\subsection*{Options}
@@ -283,9 +287,8 @@
providing a pure batch mode facility.
\medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on
-startup, instead of the primitive {\ML} top-level. This flag is usually
-enabled by default when running Isabelle via some user interface, but it is
-\emph{not} for the basic \texttt{isabelle} program.
+startup, instead of the primitive {\ML} top-level. Usually some user
+interface (such Proof~General) takes care of this flag.
\subsection*{Examples}
@@ -317,13 +320,17 @@
isabelle -r Foo
\end{ttbox}
-\medskip The next example demonstrates batch execution of Isabelle. We
-print a certain theorem of \texttt{FOL}:
+\medskip Note that manual session management like this does \emph{not} provide
+proper setup for theory presentation. This would require the \texttt{usedir}
+utility, see \S\ref{sec:tool-usedir}.
+
+\bigskip The next example demonstrates batch execution of Isabelle. We print a
+certain theorem of \texttt{FOL}:
\begin{ttbox}
isabelle -e "prth allE;" -q -r FOL
\end{ttbox}
-Note that the output text will be usually interspersed with some
-garbage produced by the {\ML} compiler.
+The output text will be usually interspersed with additional junk messages by
+the {\ML} runtime environment.
\section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool}
@@ -362,48 +369,56 @@
way for end-users to invoke a certain interface; which one to start actually
is determined by the \settdx{ISABELLE_INTERFACE} setting variable.
-Basically, there are two ways to specify an interface: either by giving an
-identifier that the Isabelle distribution knows about, or specifying an actual
-path name (containing a slash ``\texttt{/}'') of some executable. Currently,
-the following interface identifiers are recognized:
-\begin{ttdescription}
-\item[none] is just a pass-through to \texttt{isabelle}. Thus
+An interface may be specified either by giving an identifier that the Isabelle
+distribution knows about, or by specifying an actual path name (containing a
+slash ``\texttt{/}'') of some executable. Currently, the following interfaces
+are available:
+
+\begin{itemize}
+\item \texttt{none} is just a pass-through to \texttt{isabelle}. Thus
\texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.
-
-\item[xterm] refers to a simple xterm based interface which is part of
+
+\item \texttt{xterm} refers to a simple xterm based interface which is part of
the Isabelle distribution.
-\item[emacs] refers to David Aspinall's \emph{Isamode}\index{user
+\item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user
interface!Isamode} for emacs. Isabelle just provides a wrapper for this,
the actual Isamode distribution is available elsewhere \cite{isamode}.
-\end{ttdescription}
+
+\item Proof~General~\cite{proofgeneral}\index{user interface!Proof General} of
+ LFCS Edinburgh is distributed with separate interface wrapper scripts for
+ Isabelle. See below for more details.
+\end{itemize}
-The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}.
-This interface runs \texttt{isabelle} within its own xterm window.
-Usually, display of mathematical symbols from the Isabelle font is
-also enabled (see \S\ref{sec:tool-installfonts} for font configuration
-issues). Furthermore, different kinds of identifiers in logical terms
-are highlighted appropriately, e.g.\ free variables in bold and bound
-variables underlined.
-
+The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}. This
+interface runs \texttt{isabelle} within its own \textsl{xterm} window.
+Usually, display of mathematical symbols from the Isabelle font is also
+enabled (see \S\ref{sec:tool-installfonts} for font configuration issues).
+Furthermore, different kinds of identifiers in logical terms are highlighted
+appropriately, e.g.\ free variables in bold and bound variables underlined.
There are some more options available. Just pass \texttt{-?} to the
\texttt{xterm} interface to have its usage printed.
-\medskip
-
-Proof~General\index{user interface!Proof General} of LFCS Edinburgh is
-another, much more advanced interface. It supports both classic Isabelle (as
+\medskip Proof~General\index{user interface!Proof General} is a much more
+advanced interface. It supports both classic Isabelle (as
\texttt{ProofGeneral/isa}) and Isabelle/Isar (as \texttt{ProofGeneral/isar}).
Note that the latter is slightly better supported, and more robust.
-Proof~General already ships with appropriate executable scripts to be run as
-Isabelle interface. Thus a typical setup of Proof~General for Isabelle/Isar
-would be like this:
+
+Using the Isabelle interface wrapper scripts as provided by the Proof~General
+distribution, a typical setup for Isabelle/Isar would be like this:
\begin{ttbox}
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS="-p emacs -u true"
+PROOFGENERAL_OPTIONS=""
\end{ttbox}
-See \cite{proofgeneral} for more information on Proof~General.
+Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
+the Proof~General Lisp packages. There are some options available, such as
+\texttt{-l} for passing the logic image to be used.
+\medskip Note that the world may be also seen the other way round: Emacs may
+be started first (with proper Proof~General mode setup), before running
+\texttt{isabelle} from within. This requires further Emacs Lisp
+configuration, see the Proof~General documentation \cite{proofgeneral} for
+more information.
%%% Local Variables:
%%% mode: latex
--- a/doc-src/System/fonts.tex Wed Oct 13 15:41:24 1999 +0200
+++ b/doc-src/System/fonts.tex Wed Oct 13 19:39:19 1999 +0200
@@ -52,8 +52,7 @@
same machine. In this case, most X11 display servers should be happy
by being told about the Isabelle fonts directory as follows:
\begin{ttbox}
-ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
-
+ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"%$
\end{ttbox}
The same also works for remote X11 sessions in a somewhat homogeneous
network, where any X11 display machine also mounts the Isabelle
@@ -134,7 +133,6 @@
scripts are just left in plain \textsc{ascii}. Thus users with
\textsc{ascii}-only facilities will still be able to read your files.
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
--- a/doc-src/System/misc.tex Wed Oct 13 15:41:24 1999 +0200
+++ b/doc-src/System/misc.tex Wed Oct 13 19:39:19 1999 +0200
@@ -210,84 +210,6 @@
\texttt{make} invocation.
-\section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir}
-
-The \tooldx{usedir} utility builds object-logic images, or runs
-example sessions based on existing logics. Its usage is:
-\begin{ttbox}
-Usage: usedir LOGIC NAME
-
- Options are:
- -B build mode with THIS_IS_ISABELLE_BUILD indication
- -P PATH set path for remote theory browsing information
- -b build mode (output heap image, using current dir)
- -i BOOL generate theory browsing information,
- i.e. HTML / graph data (default false)
- -r reset session path
- -s NAME override session NAME
-
- Build object-logic or run examples. Also creates browsing
- information (HTML etc.) according to settings.
-
- ISABELLE_USEDIR_OPTIONS=
-\end{ttbox}
-
-Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
-implicitly prefixed to \emph{any} \texttt{usedir} call. Since the
-\ttindex{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 is enabled or
-disabled this way.
-
-
-\subsection*{Options}
-
-Basically, there are two different modes of operation: \emph{build
- mode} (enabled through the \texttt{-b} option) and \emph{example
- mode} (default).
-
-Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with input
-image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command
-line. This will be a batch session, running \texttt{ROOT.ML} from the current
-directory and then quitting. It is assumed that \texttt{ROOT.ML} contains all
-{\ML} commands required to build the logic. The \texttt{-B} option is like
-\texttt{-b}, but also indicates \texttt{THIS_IS_ISABELLE_BUILD=true} via the
-process environment. This usually causes the \texttt{ISABELLE\_OUTPUT} and
-\texttt{ISABELLE_BROWSER_INFO} settings to refer to some location within the
-Isabelle distribution directory, rather than the user's home directory.
-
-In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC}
-(typically just built before) and automatically runs \texttt{ROOT.ML} from
-within directory \texttt{NAME}. It assumes that file \texttt{ROOT.ML} in
-directory \texttt{NAME} contains appropriate {\ML} commands to run the desired
-examples.
-
-\medskip The \texttt{-i} option controls theory browsing data generation. It
-may be explicitly turned on or off --- the last occurrence of \texttt{-i} on
-the command line wins. The \texttt{-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.
-
-\medskip Any \texttt{usedir} session is named by some \emph{session
- identifier}. These accumulate, documenting the way sessions depend
-on others. For example, consider \texttt{Pure/FOL/ex}, which refers to
-the examples of {\FOL} which is built upon {\Pure}.
-
-The current session's identifier is by default just the base name of
-the \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME}
-argument (in example mode). This may be overridden explicitely via the
-\texttt{-s} option.
-
-
-\subsection*{Examples}
-
-Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
-object-logics as a model for your own developements. For example, see
-\texttt{src/FOL/IsaMakefile}.
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
--- a/doc-src/System/present.tex Wed Oct 13 15:41:24 1999 +0200
+++ b/doc-src/System/present.tex Wed Oct 13 19:39:19 1999 +0200
@@ -3,15 +3,28 @@
\chapter{Presenting theories}
+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
+structure of sessions is that of a tree, with Isabelle \texttt{Pure} at its
+root, further derived object-logics (e.g.\ \texttt{HOLCF} from \texttt{HOL},
+and \texttt{HOL} from \texttt{Pure}), and application sessions at its leaves.
+The latter usually do not have a separate {\ML} image.
+
+The \texttt{usedir} utility (see \S\ref{sec:tool-usedir}) provides the prime
+means for managing Isabelle sessions, including proper setup for presentation.
+
+
\section{Generating theory browsing information} \label{sec:info}
\index{theory browsing information|bold}
-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
-hierarchic structure of Isabelle's logics.
+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 tree structure of Isabelle's
+logics.
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
@@ -22,24 +35,31 @@
\medskip
-To generate theory browsing information for logics that are part of the
-Isabelle distribution, simply append ``\texttt{-i true}'' to the
-\settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic. For example,
-in order to do this for {\FOL}, first add something like this to your Isabelle
-settings file
+In order to let Isabelle generate theory browsing information for logics that
+are part of the Isabelle distribution, simply append ``\texttt{-i true}'' to
+the \settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic. For
+example, in order to do this for {\FOL}, add something like this to your
+Isabelle settings file
\begin{ttbox}
ISABELLE_USEDIR_OPTIONS="-i true"
\end{ttbox}
and then change into the \texttt{src/FOL} directory of the Isabelle
distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
-\medskip
+Some sessions (such as \texttt{HOL/Isar_examples}) even provide actual
+printable documents. These are prepared automatically as well if enabled by
+giving an appropriate \texttt{-d} option, e.g.\
+\begin{ttbox}
+ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
+\end{ttbox}
+See \S\ref{sec:tool-document} for further information on Isabelle document
+preparation.
-The theory browsing information is stored within the directory determined by
-the \settdx{ISABELLE_BROWSER_INFO} setting. The \texttt{index.html} file
-located there provides an entry point to all standard Isabelle logics. A
-complete HTML version of all object-logics and examples of the Isabelle
-distribution is available at
+\bigskip The theory browsing information is stored within the directory
+determined by the \settdx{ISABELLE_BROWSER_INFO} setting. The
+\texttt{index.html} file located there provides an entry point to all standard
+Isabelle logics. A complete HTML version of all object-logics and examples of
+the Isabelle distribution is available at
\begin{center}\small
\begin{tabular}{l}
\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
@@ -51,9 +71,9 @@
The generated HTML document of any theory includes all theorems proved in the
corresponding {\ML} file, provided these have been stored properly via
-\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm}, or
-\ttindex{store_thm}. Section headings may be included in the presentation via
-the {\ML} function
+\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm},
+\ttindex{bind_thms} or \ttindex{store_thm}. Section headings may be included
+in the presentation via the {\ML} function
\begin{ttbox}\index{*section}
section: string -> unit
\end{ttbox}
@@ -78,6 +98,7 @@
\end{ttbox}
+
\section{Browsing theory graphs} \label{sec:browse}
\index{theory graph browser|bold}
@@ -99,20 +120,20 @@
When no filename is specified, the browser automatically changes to
the directory \texttt{ISABELLE_BROWSER_INFO/graph/data}.
-\medskip The applet version of the browser can be invoked by opening
-the {\tt index.html} file in the directory
-\texttt{ISABELLE_BROWSER_INFO} from your Web browser and selecting
-``version for Java capable browsers''. There is also a link to the
-corresponding theory graph in every logic's {\tt index.html} file.
+\medskip The applet version of the browser can be invoked by opening the {\tt
+ index.html} file in the directory \texttt{ISABELLE_BROWSER_INFO} from your
+Web browser and selecting ``version for Java capable browsers''. There is
+also a link to the corresponding theory graph in every logic's {\tt
+ index.html} file.
\subsection{Using the graph browser}
The browser's main window, which is shown in figure
-\ref{browserwindow}, consists of two subwindows: In the left
-subwindow, the directory tree is displayed. The graph itself is
-displayed in the right subwindow.
-\begin{figure}[h]
+\ref{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{browserwindow} Browser main window}
\end{figure}
@@ -126,16 +147,16 @@
\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 subwindow, the names of
+ 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 colour.
+ 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
- subwindow.
+ sub-window.
\item Blue arrows stand before ordinary node (i.e.~theory) names. When
clicking on such a name, the graph display window focuses to the
@@ -150,7 +171,7 @@
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 colour then changes to red, indicating that
+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 ``{\tt [....]}''. To
uncollapse the nodes again, simply click on the red arrow or on the
@@ -215,6 +236,181 @@
\end{description}
+\section{Preparing Isabelle session documents --- \texttt{isatool document}}
+\label{sec:tool-document}
+
+The \tooldx{document} utility prepares logic session documents, processing the
+combined sources as provided by the user and generated by Isabelle. Its usage is:
+\begin{ttbox}
+Usage: document [OPTIONS] [DIR]
+
+ Options are:
+ -o FORMAT specify output format: dvi (default), dvi.gz, ps,
+ ps.gz, pdf
+
+ Prepare the theory session document in DIR (default '.')
+ producing the specified output format.
+\end{ttbox}
+This tool is usually run automatically as part of the corresponding session,
+provided document preparation is enabled (cf.\ the \texttt{-d} option of the
+\texttt{usedir} utility, \S\ref{sec:tool-usedir}). It may be manually invoked
+on the generated browser information document output as well.
+
+\medskip Document preparation requires a properly setup ``\texttt{document}''
+directory within the logic session sources. This directory is supposed to
+contain all the files needed to produce the actual document, apart from the
+actual theories as generated by Isabelle.
+
+\medskip For simple documents, the \texttt{document} tool is smart enough to
+create any of the output formats, taking \texttt{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
+\texttt{root.bib} within the same directory).
+
+For complex documents, a separate \texttt{IsaMakefile} may be given instead.
+It should provide targets for any admissible document format; these have to
+produce corresponding output files named after \texttt{root} as well, e.g.\
+\texttt{root.dvi} for target format \texttt{dvi}.
+
+\medskip When running the session, Isabelle copies the original
+\texttt{document} directory into its proper place within
+\texttt{ISABELLE_BROWSER_INFO} according to the session path. Then, for any
+processed theory $A$ some {\LaTeX} source is generated and put there as
+$A$\texttt{.tex}. Furthermore, a list of all generated theory files is put
+into \texttt{session.tex}. Typically, the root {\LaTeX} file provided by the
+user would include \texttt{session.tex} to get a document containing all the
+theories.
+
+The {\LaTeX} versions of the theories require some macros defined in
+\texttt{isabelle.sty} as distributed with Isabelle. Doing
+\verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
+the underlying Isabelle \texttt{latex} utility already includes an appropriate
+{\TeX} inputs path. For proper setup of hyperlinks and bookmarks in PDF
+documents we recommend to include \verb,pdfsetup.sty, as well.\footnote{It is
+ safe to do so even without using PDF~\LaTeX.}
+
+\medskip As a final step, \texttt{isatool document} is run on the resulting
+\texttt{document} directory. Thus the actual output document is built and
+installed in its proper place (as linked by the session's
+\texttt{index.html}). Note that the generated sources are left as is. While
+they may be safely deleted afterwards, this is \emph{not} done automatically.
+
+
+\section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}
+\label{sec:tool-latex}
+
+The \tooldx{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, or bbl
+
+ 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: \texttt{latex}, \texttt{pdflatex}, \texttt{bibtex},
+\texttt{dvips}. The actual commands are determined from the settings
+environment (see \texttt{ISABELLE_LATEX} etc.).
+
+It is important to note that the {\LaTeX} inputs file space has to be properly
+setup to include the Isabelle styles. Usually, this may be done by modifying
+the \settdx{TEXINPUTS} variable in settings like this:
+\begin{ttbox}
+TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
+\end{ttbox}
+This is known to work with recent versions of the \textsl{teTeX} distribution.
+
+
+
+\section{Managing logic sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
+
+The \tooldx{usedir} utility builds object-logic images, or runs example
+sessions based on existing logics. Its usage is:
+\begin{ttbox}
+Usage: usedir LOGIC NAME
+
+ Options are:
+ -B build mode with THIS_IS_ISABELLE_BUILD indication
+ -P PATH set path for remote theory browsing information
+ -b build mode (output heap image, using current dir)
+ -d FORMAT build document as FORMAT (default false)
+ -i BOOL generate theory browsing information,
+ i.e. HTML / graph data (default false)
+ -r reset session path
+ -s NAME override session NAME
+
+ Build object-logic or run examples. Also creates browsing
+ information (HTML etc.) according to settings.
+
+ ISABELLE_USEDIR_OPTIONS=
+\end{ttbox}
+
+Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
+implicitly prefixed to \emph{any} \texttt{usedir} call. Since the
+\ttindex{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 this way.
+
+
+\subsection*{Options}
+
+Basically, there are two different modes of operation: \emph{build
+ mode} (enabled through the \texttt{-b} option) and \emph{example
+ mode} (default).
+
+Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with input
+image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command
+line. This will be a batch session, running \texttt{ROOT.ML} from the current
+directory and then quitting. It is assumed that \texttt{ROOT.ML} contains all
+{\ML} commands required to build the logic. The \texttt{-B} option is like
+\texttt{-b}, but also indicates \texttt{THIS_IS_ISABELLE_BUILD=true} via the
+process environment. This usually causes the \texttt{ISABELLE\_OUTPUT} and
+\texttt{ISABELLE_BROWSER_INFO} settings to refer to some location within the
+Isabelle distribution directory, rather than the user's home directory.
+
+In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC}
+(typically just built before) and automatically runs \texttt{ROOT.ML} from
+within directory \texttt{NAME}. It assumes that file \texttt{ROOT.ML} in
+directory \texttt{NAME} contains appropriate {\ML} commands to run the desired
+examples.
+
+\medskip The \texttt{-i} option controls theory browsing data generation. It
+may be explicitly turned on or off --- the last occurrence of \texttt{-i} on
+the command line wins. The \texttt{-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.
+
+\medskip The \texttt{-d} option controls document preparation. Valid
+arguments are \texttt{false} (do not prepare document; this is default), or
+any of \texttt{dvi}, \texttt{dvi.gz}, \texttt{ps}, \texttt{ps.gz},
+\texttt{pdf}. The logic session has to provide a properly setup
+\texttt{document} directory. See \S\ref{sec:tool-document} and
+\S\ref{sec:tool-latex} for more details.
+
+\medskip Any \texttt{usedir} session is named by some \emph{session
+ identifier}. These accumulate, documenting the way sessions depend
+on others. For example, consider \texttt{Pure/FOL/ex}, which refers to
+the examples of {\FOL} which is built upon {\Pure}.
+
+The current session's identifier is by default just the base name of
+the \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME}
+argument (in example mode). This may be overridden explicitely via the
+\texttt{-s} option.
+
+
+\subsection*{Examples}
+
+Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
+object-logics as a model for your own developments. For example, see
+\texttt{src/FOL/IsaMakefile}.
+
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
--- a/doc-src/System/system.tex Wed Oct 13 15:41:24 1999 +0200
+++ b/doc-src/System/system.tex Wed Oct 13 19:39:19 1999 +0200
@@ -26,9 +26,9 @@
\pagenumbering{roman} \tableofcontents \clearfirst
\include{basics}
-\include{misc}
+\include{present}
\include{fonts}
-\include{present}
+\include{misc}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing