--- a/doc-src/System/Makefile Tue Dec 11 15:04:17 2001 +0100
+++ b/doc-src/System/Makefile Tue Dec 11 15:36:28 2001 +0100
@@ -12,7 +12,7 @@
include ../Makefile.in
NAME = system
-FILES = system.tex basics.tex misc.tex fonts.tex present.tex symbols.tex \
+FILES = system.tex basics.tex misc.tex present.tex symbols.tex \
../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
OUTPUT = syms.tex
--- a/doc-src/System/basics.tex Tue Dec 11 15:04:17 2001 +0100
+++ b/doc-src/System/basics.tex Tue Dec 11 15:36:28 2001 +0100
@@ -5,46 +5,46 @@
This manual describes Isabelle together with related tools and user interfaces
as seen from an outside (system oriented) view. See also the \emph{Isabelle
- Reference Manual}~\cite{isabelle-ref} and the \emph{Isabelle Isar Reference
- Manual}~\cite{isabelle-isar-ref} for the actual Isabelle commands and
+ 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 is based on a few general elements:
+\medskip The Isabelle system environment emerges from a few general concepts.
\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 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.
-\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.
-\item The \emph{Isabelle interface wrapper} (\ttindex{Isabelle}\footnote{Note
- the capital \texttt{I}!}), which provides some abstraction over the actual
- user interface to be used.
+\item The \emph{Isabelle settings mechanism} provides environment variables to
+ all Isabelle programs (including tools and user interfaces).
+\item The \emph{Isabelle tools wrapper} (\ttindex{isatool}) provides a generic
+ startup platform for Isabelle related utilities. Thus tools automatically
+ benefit from the settings mechanism.
+\item The raw \emph{Isabelle process} (\ttindex{isabelle} or
+ \texttt{isabelle-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} (\ttindex{Isabelle} or
+ \texttt{isabelle-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 one of the interfaces (by
-invoking the capital \texttt{Isabelle}), and maybe some basic tools like
-\texttt{doc} (see \S\ref{sec:tool-doc}). This assumes that the system has
-already been installed, of course.\footnote{In case you have to do this
- yourself, see the \ttindex{INSTALL} file in the top-level directory of the
- distribution of how to proceed. Some binary packages are available as
- well.}
+\medskip The beginning user would probably just run a standard user interface
+(by invoking the capital \texttt{Isabelle}). This assumes that the system has
+already been installed, of course. In case you have to do this yourself, see
+the \ttindex{INSTALL} file in the top-level directory of the distribution of
+how to proceed; binary packages for various system components are available as
+well.
\section{Isabelle settings} \label{sec:settings}
The Isabelle system heavily depends on the \emph{settings
- mechanism}\indexbold{settings}. Basically, this is a statically scoped
+ mechanism}\indexbold{settings}. Essentially, this is a statically scoped
collection of environment variables, such as \texttt{ISABELLE_HOME},
\texttt{ML_SYSTEM}, \texttt{ML_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 plain shell environment variables.
+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
@@ -55,10 +55,10 @@
not required.}
-\subsection{Building the environment}
+\subsection{Constructing the environment}
Whenever any of the Isabelle executables is run, their settings environment is
-built as follows.
+put together as follows.
\begin{enumerate}
\item The special variable \settdx{ISABELLE_HOME} is determined automatically
@@ -76,8 +76,8 @@
This file typically contains 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 have to
- be adapted (most likely \texttt{ML_SYSTEM} etc.).
+ for most variables. When installing the system, only a few of these may have
+ to be adapted (probably \texttt{ML_SYSTEM} etc.).
\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is
run in the same way as the site default settings. Note that the variable
@@ -102,17 +102,17 @@
\medskip A few variables are somewhat special:
\begin{itemize}
-\item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to
- the absolute path names of the \texttt{isabelle} and
- \texttt{isatool} executables, respectively.
+\item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to the
+ absolute path names of the \texttt{isabelle-process} and \texttt{isatool}
+ executables, respectively.
-\item \settdx{ISABELLE_OUTPUT} will has the {\ML} system identifier (according
- to \texttt{ML_IDENTIFIER}) automatically appended to its value.
+\item \settdx{ISABELLE_OUTPUT} will have the {\ML} system identifier
+ (according to \texttt{ML_IDENTIFIER}) automatically appended to its value.
\end{itemize}
-\medskip The Isabelle settings scheme is basically simple, but non-trivial.
-For debugging purposes, the resulting environment may be inspected with the
-\texttt{getenv} utility, see \S\ref{sec:tool-getenv}.
+\medskip The Isabelle settings scheme is conceptually simple, but not
+completely trivial. For debugging purposes, the resulting environment may be
+inspected with the \texttt{getenv} utility, see \S\ref{sec:tool-getenv}.
\subsection{Common variables}
@@ -124,8 +124,8 @@
\begin{description}
\item[\settdx{ISABELLE_HOME}*] is the location of the top-level Isabelle
distribution directory. This is automatically determined from the Isabelle
- executable that has been invoked. Do not try to set \texttt{ISABELLE_HOME}
- yourself from the shell.
+ executable that has been invoked. Do not attempt to set
+ \texttt{ISABELLE_HOME} yourself from the shell.
\item[\settdx{ISABELLE_HOME_USER}] is the user-specific counterpart of
\texttt{ISABELLE_HOME}. The default value is \texttt{\~\relax/isabelle},
@@ -135,9 +135,10 @@
be overridden by a private \texttt{etc/settings}.
\item[\settdx{ISABELLE}*, \settdx{ISATOOL}*] are automatically set to the full
- path names of the \texttt{isabelle} and \texttt{isatool} executables,
- respectively. Thus other tools and scripts need not assume that the
- Isabelle \texttt{bin} directory is on the current search path of the shell.
+ path names of the \texttt{isabelle-process} and \texttt{isatool}
+ executables, respectively. Thus other tools and scripts need not assume
+ that the Isabelle \texttt{bin} directory is on the current search path of
+ the shell.
\item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS},
\settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML}
@@ -188,27 +189,70 @@
\item[\settdx{DVI_VIEWER}] specifies the command to be used for displaying
\texttt{dvi} files.
-\item[\settdx{ISABELLE_INSTALL_FONTS}] determines the way that the Isabelle
- symbol fonts are installed into your currently running X11 display server.
- X11 fonts are a subtle issue, see \S\ref{sec:tool-installfonts} for more
- information.
-
-\item[\settdx{ISABELLE_TMP_PREFIX}] is the prefix from which any running
+\item[\settdx{ISABELLE_TMP_PREFIX}*] is the prefix from which any running
\texttt{isabelle} process derives an individual directory for temporary
files. The default is somewhere in \texttt{/tmp}.
\item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the actual
- user interface that the capital \texttt{Isabelle} should invoke. See
- \S\ref{sec:interface} for more details.
+ user interface that the capital \texttt{Isabelle} or
+ \texttt{isabelle-interface} should invoke. See \S\ref{sec:interface} for
+ more details.
\end{description}
-\section{Isabelle proper --- \texttt{isabelle}}
+\section{The Isabelle tools wrapper} \label{sec:isatool}
+
+All Isabelle related utilities are called via a common wrapper ---
+\ttindex{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 \S\ref{sec:settings}. The set
+of available tools is collected by \texttt{isatool} from the directories
+listed in the \texttt{ISABELLE_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!
+
+
+\subsubsection*{Examples}
-The \ttindex{isabelle} executable runs bare-bones 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:
+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 \S\ref{sec:tool-mkdir}
+and \S\ref{sec:tool-make}):
+\begin{ttbox}
+ isatool mkdir HOL Test && isatool make
+\end{ttbox}
+Note that \texttt{isatool mkdir} is usually only invoked once; existing
+sessions (including document output etc.) are then updated by \texttt{isatool
+ make} alone.
+
+
+\section{The raw Isabelle process}
+
+The \ttindex{isabelle} (or \ttindex{isabelle-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]
@@ -244,15 +288,15 @@
If the input heap file does not have write permission bits set, or the
\texttt{-r} option is given explicitely, then the session started will be
-read-only. That is, the {\ML} world cannot be committed back into the logic
-image. Otherwise, a writable session enables commits into either the input
+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 an alternative output heap file (in case 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. Users are responsible themselves to dispose their heap
-files when they are no longer needed.
+amounts of disk space (approximately 20--40~MB). Users are responsible for
+themselves to dispose their heap files when they are no longer needed.
\medskip The \texttt{-w} option makes the output heap file read-only after
terminating. Thus subsequent invocations cause the logic image to be
@@ -260,8 +304,8 @@
\medskip The \texttt{-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 values maximally shared, resulting in up to 50\%
-less disk space consumption.
+garbage collected and all stored values are maximally shared, resulting in up
+to 50\% less disk space consumption.
\medskip The \texttt{-C} option tells the ML system to produce a completely
self-contained output image, probably including a copy of the ML runtime
@@ -280,7 +324,7 @@
\medskip The \texttt{-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 mathematical symbols from a special screen font.
+to enable output of proper mathematical symbols.
\medskip Isabelle normally enters an interactive top-level loop (after
processing the \texttt{-e} texts). The \texttt{-q} option inhibits
@@ -307,9 +351,8 @@
\begin{ttbox}
isabelle FOL Foo
\end{ttbox}
-Ending this session normally (e.g.\ by typing control-D) dumps the
-whole {\ML} system state into \texttt{Foo}. Be prepared for several
-megabytes!
+Ending this session normally (e.g.\ by typing control-D) dumps the whole {\ML}
+system state into \texttt{Foo}. Be prepared for several tens of megabytes.
The \texttt{Foo} session may be continued later (still in writable
state) by:
@@ -334,38 +377,14 @@
by the {\ML} runtime environment.
-\section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool}
-
-All Isabelle related utilities are called via a common wrapper ---
-\ttindex{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
- doc - view Isabelle documentation
- \dots
-\end{ttbox}
-Basically, Isabelle tools are ordinary executable scripts. These are run
-within the same Isabelle settings environment, see \S\ref{sec:settings}. The
-set of available tools is collected by \texttt{isatool} from the directories
-listed in the \texttt{ISABELLE_TOOLS} setting. Do not try to call the scripts
-directly. Neither should you add the tool directories to your shell's search
-path.
-
-
-\section{The Isabelle interface wrapper --- \texttt{Isabelle}} \label{sec:interface}
+\section{The Isabelle interface wrapper}\label{sec:interface}
Isabelle is a generic theorem prover, even w.r.t.\ its user interface. The
-\ttindex{Isabelle} command (note the capital \texttt{I}) provides a uniform
-way for end-users to invoke a certain interface; which one to start actually
-is determined by the \settdx{ISABELLE_INTERFACE} setting variable. Also note
-that the \texttt{install} utility provides some options to install desktop
-environment icons as well (see \S\ref{sec:tool-install}).
+\ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
+uniform way for end-users to invoke a certain interface; which one to start
+actually is determined by the \settdx{ISABELLE_INTERFACE} setting variable.
+Also note that the \texttt{install} utility provides some options to install
+desktop environment icons as well (see \S\ref{sec:tool-install}).
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
@@ -373,21 +392,10 @@
are available:
\begin{itemize}
-\item \texttt{none} is just a pass-through to plain \texttt{isabelle}. Thus
+\item \texttt{none} is just a pass-through to raw \texttt{isabelle}. Thus
\texttt{Isabelle} basically becomes an alias for \texttt{isabelle}. This is
the factory default.
-\item \texttt{xterm} refers to a simple \textsl{xterm} based interface which
- is part of the Isabelle distribution.
-
- This interface runs \texttt{isabelle} within its own \textsl{xterm} window.
- Usually, display of mathematical symbols from the Isabelle font is enabled
- as well (see \S\ref{sec:tool-installfonts} for X11 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 get the usage printed.
-
\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}.
@@ -406,8 +414,10 @@
\end{ttbox}
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, or \texttt{-m} to tune
- the standard print mode.
+ \texttt{-l} for passing the logic image to be used by default, or
+ \texttt{-m} to tune the standard print mode. The \texttt{-I} option allows
+ to switch between the Isar and ML view, independently of the actual
+ 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
--- a/doc-src/System/misc.tex Tue Dec 11 15:04:17 2001 +0100
+++ b/doc-src/System/misc.tex Tue Dec 11 15:36:28 2001 +0100
@@ -24,8 +24,8 @@
The resulting theory text uses the tactic emulation facilities of
Isabelle/Isar (see also \cite{isabelle-ref}, especially the ``Conversion
guide'' in the appendix). Usually there is some manual tuning required to get
-an automatically converted script work again --- the success rate may be
-around 99\% for common ML scripts.
+an automatically converted script work again --- the success rate is around
+99\% for common ML scripts.
\section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc}
@@ -82,7 +82,7 @@
available.
-\section{Inspecting the settings environment -- \texttt{isatool getenv}}
+\section{Inspecting the settings environment --- \texttt{isatool getenv}}
\label{sec:tool-getenv}
The Isabelle settings environment --- as provided by the site-default and
@@ -130,7 +130,7 @@
path component. This is a special feature of \texttt{ISABELLE_OUTPUT}.
-\section{Installing standalone Isabelle executables -- \texttt{isatool install}}
+\section{Installing standalone Isabelle executables --- \texttt{isatool install}}
\label{sec:tool-install}
By default, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool} etc.)
@@ -167,7 +167,7 @@
The icon will appear directly on the desktop.
-\section{Creating instances of the Isabelle logo -- \texttt{isatool
+\section{Creating instances of the Isabelle logo --- \texttt{isatool
logo}}
The \tooldx{logo} utility creates any instance of the generic Isabelle logo as
@@ -219,7 +219,7 @@
\texttt{src/FOL/IsaMakefile}.
-\section{Make all logics -- \texttt{isatool makeall}}
+\section{Make all logics --- \texttt{isatool makeall}}
The \tooldx{makeall} utility applies Isabelle make to all logic
directories of the distribution:
@@ -231,6 +231,24 @@
The arguments \texttt{ARGS} are just passed verbatim to each
\texttt{make} invocation.
+
+\section{Remove awkward symbol names from theory sources --- \texttt{isatool unsymbolize}}
+
+The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve
+readability for plain ASCII output (e.g.\ in email communication). Most
+notably, \texttt{unsymbolize} replaces awkward arrow symbols such as
+\verb|\<Longrightarrow>| by \verb|==>|.
+\begin{ttbox}
+Usage: unsymbolize [FILES|DIRS...]
+
+ Recursively find .thy/.ML files, removing unreadable symbol names.
+ Note: this is an ad-hoc script; there is no systematic way to replace
+ symbols independently of the inner syntax of a theory!
+
+ Renames old versions of FILES by appending "~~".
+\end{ttbox}
+
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
--- a/doc-src/System/present.tex Tue Dec 11 15:04:17 2001 +0100
+++ b/doc-src/System/present.tex Tue Dec 11 15:36:28 2001 +0100
@@ -6,21 +6,40 @@
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 \texttt{Pure} at its
-root, further object-logics derived (e.g.\ \texttt{HOLCF} from \texttt{HOL},
-and \texttt{HOL} from \texttt{Pure}), and application sessions in leaf
-positions. The latter usually do not have a separate {\ML} image.
+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 \texttt{mkdir} (see \S\ref{sec:tool-mkdir}) and \texttt{make} (see
\S\ref{sec:tool-make}) tools of Isabelle provide the primary means for
managing Isabelle sessions, including proper setup for presentation. Here the
-\texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to run any
-additional stages required for document preparation, notably the tools
-\texttt{document} (see \S\ref{sec:tool-document}) and \texttt{latex} (see
-\S\ref{sec:tool-latex}).
+\texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to let the
+\texttt{isabelle} process run any additional stages required for document
+preparation, notably the tools \texttt{document} (see
+\S\ref{sec:tool-document}) and \texttt{latex} (see \S\ref{sec:tool-latex}).
+The complete tool chain for managing batch-mode Isabelle sessions is
+illustrated in figure~\ref{fig:session-tools}.
+
+\begin{figure}[htbp]
+ \begin{center}
+ \begin{tabular}{lp{0.6\textwidth}}
+ \texttt{isatool mkdir} & invoked once by the user to create the initial
+ source setup (common \texttt{IsaMakefile} plus a single session directory); \\
+ \texttt{isatool make} & invoked repeatedly by the user to
+ keep session output up-to-date (HTML, documents etc.); \\
+ \texttt{isatool usedir} & part of the standard \texttt{IsaMakefile} entry of a session; \\
+ \texttt{isabelle} & run through \texttt{isatool usedir}; \\
+ \texttt{isatool document} & run by the Isabelle process if document preparation is enabled; \\
+ \texttt{isatool latex} & universal {\LaTeX} tool wrapper invoked multiple times
+ by \texttt{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}
-\section{Generating theory browsing information} \label{sec:info}
+\section{Generating theory browser information} \label{sec:info}
\index{theory browsing information|bold}
As a side-effect of running a logic sessions, Isabelle is able to generate
@@ -34,36 +53,44 @@
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 browser first. The latter version also includes
+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 \S\ref{sec:browse} for further information.
\medskip
-In order to let Isabelle generate theory browsing information, 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 this to your
-Isabelle settings file
+The easiest way to let Isabelle generate theory browsing information for
+existing sessions is to append ``\texttt{-i true}'' to the
+\settdx{ISABELLE_USEDIR_OPTIONS} before invoking \texttt{isatool make} (or
+\texttt{./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 \texttt{src/FOL} directory of the Isabelle
distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
+The presentation output will appear in \texttt{\$ISABELLE_BROWSER_INFO/FOL},
+which usually refers to \verb,~/isabelle/browser_info/FOL,. Note that option
+\texttt{-v true} will make the internal runs of \texttt{usedir} more explicit
+about such details.
-Some sessions (such as \texttt{HOL/Isar_examples}) even provide actual
+Many standard Isabelle sessions (such as \texttt{HOL/ex}) also provide actual
printable documents. These are prepared automatically as well if enabled like
this, using the \texttt{-d} option
\begin{ttbox}
ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
\end{ttbox}
-See \S\ref{sec:tool-document} for further information on Isabelle document
-preparation.
+Enabling options \texttt{-i} and \texttt{-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 \S\ref{sec:tool-document} for further details.
-\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
+\bigskip The theory browsing information is stored in a sub-directory
+directory determined by the \settdx{ISABELLE_BROWSER_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/} \\
@@ -71,31 +98,19 @@
\end{tabular}
\end{center}
-\medskip
-
-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},
-\ttindex{bind_thms} or \ttindex{store_thm} (see also \cite{isabelle-ref}).
-Section headings may be included in the presentation via the {\ML} function
-\begin{ttbox}\index{*section}
-section: string -> unit
-\end{ttbox}
-
-\medskip
-
-In order to present your own theories on the web, simply copy the
+\medskip In order to present your own theories on the web, simply copy the
corresponding subdirectory from \texttt{ISABELLE_BROWSER_INFO} to your WWW
-server, after having generated browser info like this:
+server, having generated browser info like this:
\begin{ttbox}
isatool usedir -i true HOL Foo
\end{ttbox}
This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
-to load all your theories, and HOL is your parent logic image. Ideally,
-theory browser information would have been generated for HOL already.
-
-Alternatively, one may specify an external link to an existing body of HTML
-data by giving \texttt{usedir} a \texttt{-P} option like this:
+to load all your theories, and HOL is your parent logic image (\texttt{isatool
+ mkdir} assists in setting up Isabelle session directories, see
+\S\ref{sec:tool-mkdir}). 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 \texttt{usedir} a \texttt{-P}
+option like this:
\begin{ttbox}
isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
\end{ttbox}
@@ -105,8 +120,7 @@
There is a separate \texttt{mkdir} tool to provide easy setup of all this,
with only minimal manual editing required.
\begin{ttbox}
-isatool mkdir Foo
-isatool make
+isatool mkdir HOL Foo && isatool make
\end{ttbox}
See \S\ref{sec:tool-mkdir} for more information on preparing Isabelle session
directories, including the setup for documents.
@@ -115,11 +129,14 @@
\section{Browsing theory graphs} \label{sec:browse}
\index{theory graph browser|bold}
-The graph browser is a 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 filter out irrelevant
-information. The browser is written in Java, it can be used both as a
-stand-alone application and as an applet.
+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 \texttt{-g} of \texttt{isatool usedir} (see
+\S\ref{sec:tool-usedir}) creates graph presentations in batch mode for
+inclusion in session documents.
\subsection{Invoking the graph browser}
@@ -145,12 +162,12 @@
\subsection{Using the graph browser}
The browser's main window, which is shown in figure
-\ref{browserwindow}, consists of two sub-windows: In the left
+\ref{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{browserwindow} Browser main window}
+ \caption{\label{fig:browserwindow} Browser main window}
\end{figure}
@@ -205,7 +222,7 @@
\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 paper. The resulting
+ 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
@@ -250,115 +267,6 @@
\end{description}
-\section{Preparing Isabelle session documents --- \texttt{isatool document}}
-\label{sec:tool-document}
-
-The \tooldx{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
- -o FORMAT specify output format: dvi (default), dvi.gz, ps,
- ps.gz, pdf
- -v be verbose
-
- 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 session,
-provided document preparation has been 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 final document --- apart from the
-actual theories which are 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.
-
-If the text contains any references to Isabelle symbols (such as
-\verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
-This package contains a standard set of {\LaTeX} macro definitions
-\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see
-Appendix~\ref{app:symbols} for a complete list). The user may refer to
-further symbols as well, simply by providing {\LaTeX} macros of the same sort.
-
-For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
-images), we recommend to include \verb,pdfsetup.sty, as well. It is safe to
-do so even without using PDF~\LaTeX.
-
-\medskip As a final step, \texttt{isatool document -c} 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}). The generated sources are deleted after successful run
-of {\LaTeX} and friends. Note that a copy of the sources may be retained by
-passing an option \texttt{-D} to the \texttt{usedir} utility when running the
-session (see also \S\ref{sec:tool-usedir}).
-
-
-\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, bbl, png, sty
-
- 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{dvips},
-\texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
-The actual commands are determined from the settings environment
-(\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
-
-The \texttt{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 \texttt{-D} of the \texttt{usedir} utility, see
-\S\ref{sec:tool-usedir}).
-
-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{Creating Isabelle session directories --- \texttt{isatool mkdir}}
\label{sec:tool-mkdir}
@@ -367,7 +275,7 @@
and a \texttt{document} directory with a minimal \texttt{root.tex} that is
sufficient print all theories of the session (in the order of appearance); see
\S\ref{sec:tool-document} for further information on Isabelle document
-preparation. The usage of \texttt{mkdir} is:
+preparation. The usage of \texttt{isatool mkdir} is:
\begin{ttbox}
Usage: mkdir [OPTIONS] [LOGIC] NAME
@@ -383,7 +291,7 @@
The \texttt{mkdir} tool is conservative in the sense that any existing
\texttt{IsaMakefile} etc.\ is left unchanged. Thus it is safe to invoke it
-experimentally, with varying options.
+multiple times, although later runs may not have the desired effect.
Note that \texttt{mkdir} is unable to change \texttt{IsaMakefile}
incrementally --- manual changes are required for multiple sub-sessions. On
@@ -420,16 +328,23 @@
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
+isatool mkdir Foo && isatool make
\end{ttbox}
\noindent The theory sources should be put into the \texttt{Foo} directory, and its
\texttt{ROOT.ML} should be edited to load all required theories. Invoking
-\texttt{isatool make} would now run the whole session, generating browser
+\texttt{isatool make} again would run the whole session, generating browser
information and the document automatically. The \texttt{IsaMakefile} is
-usually tuned manually later, e.g.\ adding actual source dependencies, or
+typically tuned manually later, e.g.\ adding actual source dependencies, or
changing the options passed to \texttt{usedir}.
+\medskip Large projects may demand further sessions, potentially with separate
+logic images being created. This usually requires manual editing of the
+generated \texttt{IsaMakefile}, which is meant to cover all of the sub-session
+directories at the same time (this is the deeper reasong why
+\texttt{IsaMakefile} is not made part of the initial session directory created
+by \texttt{isatool mkdir}). See \texttt{src/HOL/IsaMakefile} of the Isabelle
+distribution for a full-blown example.
+
\section{Running Isabelle sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
@@ -445,6 +360,7 @@
-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)
+ -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
@@ -500,6 +416,14 @@
\texttt{document} directory. See \S\ref{sec:tool-document} and
\S\ref{sec:tool-latex} for more details.
+The \texttt{-g} option produces images of the theory dependency graph (cf.\
+\S\ref{sec:browse}) for inclusion in the generated document, both as
+\texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time.
+In order to make this appear the final {\LaTeX} document one would typically
+say \verb,\includegraphics{session_graph}, in the \texttt{document/root.tex}
+file. (Omitting the file-name extension enables {\LaTeX} to select to correct
+version, either for the DVI or PDF output path.)
+
\medskip The \texttt{-D} option causes the generated document sources to be
dumped at location \texttt{PATH}, which is relative to the session's main
directory. For example, \texttt{-D document} would leave a copy of the
@@ -533,6 +457,135 @@
\S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation
of \texttt{usedir} as well.
+
+\section{Preparing Isabelle session documents --- \texttt{isatool document}}
+\label{sec:tool-document}
+
+The \tooldx{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
+ -o FORMAT specify output format: dvi (default), dvi.gz, ps,
+ ps.gz, pdf
+
+ 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
+\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, e.g.\ in case of errors encountered in the batch run.
+
+\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 final document --- apart from the
+actual theories which are generated by Isabelle.
+
+\medskip For most practical purposes, the \texttt{document} tool is smart
+enough to create any of the specified 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).
+
+In more complex situations, a separate \texttt{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
+\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.
+
+If the text contains any references to Isabelle symbols (such as
+\verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
+This package contains a standard set of {\LaTeX} macro definitions
+\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see
+Appendix~\ref{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 \texttt{isabellesym.sty} of the
+distribution.
+
+For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
+images), we recommend to include \verb,pdfsetup.sty, as well. It is safe to
+do so even without using PDF~\LaTeX.
+
+\medskip As a final step of document preparation within Isabelle,
+\texttt{isatool document -c} 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} if option
+\texttt{-i} of \texttt{usedir} has been enabled, cf.\ \S\ref{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
+\texttt{-D} to the \texttt{usedir} utility when running the session (see also
+\S\ref{sec:tool-usedir}).
+
+
+\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, bbl, png, sty
+
+ 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{dvips},
+\texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
+The actual commands are determined from the settings environment
+(\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
+
+The \texttt{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 \texttt{-D} of the \texttt{usedir} utility, see
+\S\ref{sec:tool-usedir}).
+
+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 the Isabelle settings like this:
+\begin{ttbox}
+TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
+\end{ttbox}
+This is known to work with \textsl{teTeX} (version 1.0 or later).
+
+
+\subsubsection*{Examples}
+
+Invoking \texttt{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 \texttt{ISABELLE_BROWSER_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}
+
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
--- a/doc-src/System/symbols.tex Tue Dec 11 15:04:17 2001 +0100
+++ b/doc-src/System/symbols.tex Tue Dec 11 15:36:28 2001 +0100
@@ -1,7 +1,7 @@
% $Id$
-\chapter{Isabelle symbols}\label{app:symbols}
+\chapter{Standard Isabelle symbols}\label{app:symbols}
Isabelle supports an infinite number of non-ASCII symbols, which are
represented in source text as \verb,\<,$name$\verb,>, (where $name$ may be any
--- a/doc-src/System/system.tex Tue Dec 11 15:04:17 2001 +0100
+++ b/doc-src/System/system.tex Tue Dec 11 15:36:28 2001 +0100
@@ -8,7 +8,6 @@
\usepackage[latin1]{inputenc}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{wasysym}
-\usepackage{eufrak}
\usepackage{textcomp}
\usepackage{marvosym}
\usepackage{supertabular}
@@ -40,7 +39,6 @@
\include{basics}
\include{present}
\include{misc}
-\include{fonts}
\appendix
\let\int\intorig