--- a/doc-src/System/basics.tex Mon Oct 18 18:38:21 1999 +0200
+++ b/doc-src/System/basics.tex Mon Oct 18 19:43:18 1999 +0200
@@ -1,112 +1,105 @@
% $Id$
-\chapter{Basic concepts}
+\chapter{The Isabelle system environment}
-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.
+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
+related functions.
\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 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.
- Furthermore, the shell's search path is kept clean from many small
- programs.
-\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 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.
\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 properly, of
-course.\footnote{In case you have to do this yourself, see the
- \ttindex{INSTALL} file in the top-level directory of the
- distribution. The information provided there should be sufficient as
- a start.}
+\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.}
\section{Isabelle settings} \label{sec:settings}
The Isabelle system heavily depends on the \emph{settings
- mechanism}\indexbold{settings}. Basically, this is just a collection
-of environment variables, e.g.\ \texttt{ISABELLE_HOME},
-\texttt{ML_SYSTEM}, \texttt{ML_HOME}. These variables are \emph{not}
-intended to be set directly from the shell!
+ mechanism}\indexbold{settings}. Basically, 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.
-Isabelle employs a somewhat more sophisticated scheme of
-\emph{settings files} --- one for site-wide defaults, another for
-optional user-specific modifications. With all configuration
-variables in just a few places, this is much more maintainable and
-user-friendly than ordinary shell environment variables.
-
-In particular, we avoid the typical situation where prospective users
-of a software package are told to put this and that in their shell
-startup scripts, before being able to actually run it. Isabelle
-requires none such administrative chores of its end-users --- the
-executables can be invoked straight away. Usually, users would just
-want to put the Isabelle \texttt{bin} directory into their shell's
-search path, of course.
+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 it. 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
+\texttt{bin} directory into their shell's search path, but this is not
+required.
-\subsection{Building the environment}
+\subsection{Creating the environment}
-Whenever any of the Isabelle executables is run, their settings
-environment is built as follows:
+Whenever any of the Isabelle executables is run, their settings environment is
+built as follows:
\begin{enumerate}
-\item The special variable \settdx{ISABELLE_HOME} is determined
- automatically from the location of the binary that has been run.
-
- You should not try to set \texttt{ISABELLE_HOME} manually. Also note
- that the Isabelle executables have to be run from their original
- location in the distribution directory --- copying or linking them
- somewhere else just won't work!
-
-\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a
- shell script with the auto-export option for variables enabled.
-
+\item The special variable \settdx{ISABELLE_HOME} is determined automatically
+ from the location of the binary that has been run.
+
+ You should not try to set \texttt{ISABELLE_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 via the
+ \texttt{install} utility (see \S\ref{sec:tool-install}). Just doing a plain
+ copy of the \texttt{bin} files will not work!
+
+\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script
+ with the auto-export option for variables enabled.
+
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.).
+ 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.).
\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
+ run in 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.
- Typically, a user settings file would contain only a few lines, just
- the assigments that are really needed. One should definitely
- \emph{not} start with a full copy the central
- \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very
- annoying maintainance problems later, when the Isabelle installation
- is updated or changed otherwise.
+
+ Thus individual users may override the site-wide defaults. See also file
+ \texttt{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 \texttt{\$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, say \texttt{if} or \texttt{case}
-statements to set variables depending on the system architecture or
-other environment variables, for example. Such advanced features
-should be added only with great care, though. In particular, external
-environment references should be kept at a minimum.
+Note that settings files are actually full GNU bash scripts. So one may use
+complex shell commands, such as \texttt{if} or \texttt{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}
@@ -119,111 +112,105 @@
appended to their values.
\end{itemize}
-\medskip The Isabelle settings scheme is basically quite 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 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}.
\subsection{Common variables}
-Below 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 *.
+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 *.
\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.
-
+\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.
+
\item[\settdx{ISABELLE_HOME_USER}] is the user-specific counterpart of
- \texttt{ISABELLE_HOME}. The default value is
- \texttt{\~\relax/isabelle}, under rare circumstances this may be
- changed in the global setting file. Typically, the
- \texttt{ISABELLE_HOME_USER} directory mimics \texttt{ISABELLE_HOME}
- to some extend. In particular, site-wide defaults may be overridden
- by a private \texttt{etc/settings}.
-
-\item[\settdx{ISABELLE}*, \settdx{ISATOOL}*] are automatically set to
- the full paths 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.
+ \texttt{ISABELLE_HOME}. The default value is \texttt{\~\relax/isabelle},
+ under rare circumstances this may be changed in the global setting file.
+ Typically, the \texttt{ISABELLE_HOME_USER} directory mimics
+ \texttt{ISABELLE_HOME} to some extend. In particular, site-wide defaults may
+ 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.
\item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS},
\settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML}
- system to be used for Isabelle. The choice of \texttt{ML_SYSTEM}
- identifiers is quite fixed, see the global \texttt{etc/settings} file for
- some examples. The actual compiler binary will be run from directory
- \texttt{ML_HOME}, with \texttt{ML_OPTIONS} as first arguments on the command
- line. The optional \texttt{ML_PLATFORM} specifies the binary format of ML
- heap images, which is useful for cross-platform installations. The value of
- \texttt{ML_IDENTIFIER} is (automatically) obtained by composing
- \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}.
+ system to be used for Isabelle. There is only a fixed set of admissable
+ \texttt{ML_SYSTEM} names (see the \texttt{etc/settings} file of the
+ distribution).
+
+ The actual compiler binary will be run from the directory \texttt{ML_HOME},
+ with \texttt{ML_OPTIONS} as first arguments on the command line. The
+ optional \texttt{ML_PLATFORM} may specify the binary format of ML heap
+ images, which is useful for cross-platform installations. The value of
+ \texttt{ML_IDENTIFIER} is automatically obtained by composing the
+ \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM} values.
\item[\settdx{ISABELLE_PATH}*] is a list of directories (separated by colons)
where Isabelle logic images may reside. Note that the value of
\texttt{ML_IDENTIFIER} is appended to each component automatically.
-
-\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
- files should be stored by default. The \texttt{ML_SYSTEM} identifier
- is appended here, too.
-
-\item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory
- browser information (HTML and graph data) is stored (see also
- \S\ref{sec:info}). The default value is
+
+\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap files should
+ be stored by default. The \texttt{ML_SYSTEM} identifier is appended here,
+ too.
+
+\item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory browser
+ information (HTML text, graph data, and printable documents) is stored (see
+ also \S\ref{sec:info}). The default value is
\texttt{\$ISABELLE_HOME_USER/browser_info}.
-
-\item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
- none is given explicitely by the user --- e.g.\ when running
- \texttt{isabelle} directly, or some user interface.
-
-\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the
- command line of any \texttt{isatool usedir} invocation (see also
- \S\ref{sec:tool-usedir}). This typically contains compilation
- options for object-logics --- \texttt{usedir} is the basic utility
- that builds them (cf.\ the \texttt{IsaMakefile}s in the
- distribution).
+
+\item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if none is
+ given explicitely by the user. The default value is \texttt{HOL}.
+
+\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the command
+ line of any \texttt{isatool usedir} invocation (see also
+ \S\ref{sec:tool-usedir}). This typically contains compilation options for
+ object-logics --- \texttt{usedir} is the basic utility for managing logic
+ sessions (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
- programs (see also \S\ref{sec:isatool}).
-
-\item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories
- with documentation files.
-
-\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 non-trivial issue, see
- \S\ref{sec:tool-installfonts} for more information.
-
-\item[\settdx{ISABELLE_TMP_PREFIX}] is the prefix from which any
- \texttt{isabelle} session 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. Currently available are \texttt{none}, \texttt{xterm} and
- \texttt{emacs}. See \S\ref{sec:interface} for more details.
+
+\item[\settdx{ISABELLE_TOOLS}] is a colon separated list of directories that
+ are scanned by \texttt{isatool} for external utility programs (see also
+ \S\ref{sec:isatool}).
+
+\item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories with
+ documentation files.
+
+\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
+ \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.
\end{description}
\section{Isabelle proper --- \texttt{isabelle}}
-The \ttindex{isabelle} executable runs 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:
+The \ttindex{isabelle} executable runs 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]
@@ -243,52 +230,51 @@
\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 slash
-(\texttt{/}) in the name (hint: use \texttt{./} to refer to the current
+separated by colons --- these are tried in the given 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}
If the input heap file does not have write permission bits set, or the
-\texttt{-r} option is given explicitely, then the session 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 file, or into an alternative output heap file (in
-case this is given as the second argument on the command line).
+\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
+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.
+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.
-\medskip The \texttt{-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 \texttt{-w} option makes the output heap file read-only after
+terminating. Thus subsequent invocations cause the logic image to be
+read-only automatically.
-\medskip Using the \texttt{-e} option, arbitrary {\ML} code may be
-passed to the Isabelle session from the command line. Multiple
-\texttt{-e}'s are evaluated in order. Strange things may happen when
-errorneous {\ML} code is given. Also make sure that the {\ML} commands
-are terminated properly by semicolon.
+\medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to
+the Isabelle session from the command line. Multiple \texttt{-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 \texttt{-u} option is a shortcut for \texttt{-e}, passing
``\texttt{use"ROOT.ML";}'' to the {\ML} session.
-\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, for example to enable output of mathematical symbols from a
-special screen font.
+\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.
-\medskip Isabelle normally enters an interactice top-level loop (after
-processing the \texttt{-e} texts). The \texttt{-q} option inhibits this, thus
-providing a pure batch mode facility.
+\medskip Isabelle normally enters an interactive top-level loop (after
+processing the \texttt{-e} texts). The \texttt{-q} option inhibits
+interaction, thus 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. Usually some user
-interface (such Proof~General) takes care of this flag.
+startup, instead of the primitive {\ML} top-level. User interfaces (such
+Proof~General) take care of this switch automatically.
\subsection*{Examples}
@@ -329,8 +315,8 @@
\begin{ttbox}
isabelle -e "prth allE;" -q -r FOL
\end{ttbox}
-The output text will be usually interspersed with additional junk messages by
-the {\ML} runtime environment.
+Note that the output text will be interspersed with additional junk messages
+by the {\ML} runtime environment.
\section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool}
@@ -345,21 +331,16 @@
Available tools are:
- browser - Isabelle theory graph browser
+ browser - Isabelle graph browser
doc - view Isabelle documentation
\dots
\end{ttbox}
-Basically, Isabelle tools are ordinary executable scripts. These are
-run within the same settings environment as Isabelle proper, see
-\S\ref{sec:settings}. The set of available tools is collected by
-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.
-
-
-\medskip See chapter~\ref{ch:tools} for descriptions of most utilities
-that come with the Isabelle distributions. Third-parties may add their
-own, of course.
+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}
@@ -367,7 +348,9 @@
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.
+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
@@ -375,7 +358,7 @@
are available:
\begin{itemize}
-\item \texttt{none} is just a pass-through to \texttt{isabelle}. Thus
+\item \texttt{none} is just a pass-through to plain \texttt{isabelle}. Thus
\texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.
\item \texttt{xterm} refers to a simple xterm based interface which is part of
@@ -392,8 +375,8 @@
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).
+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
@@ -402,21 +385,21 @@
\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.
+Note that the latter is inherently more robust.
-Using the Isabelle interface wrapper scripts as provided by the Proof~General
-distribution, a typical setup for Isabelle/Isar would be like this:
+Using the Isabelle interface wrapper scripts as provided by Proof~General, a
+typical setup for Isabelle/Isar would be like this:
\begin{ttbox}
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS=""
+PROOFGENERAL_OPTIONS="-u false"
\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.
\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
+be started first (with proper setup of Proof~General mode), and
+\texttt{isabelle} run from within. This requires further Emacs Lisp
configuration, see the Proof~General documentation \cite{proofgeneral} for
more information.
--- a/doc-src/System/fonts.tex Mon Oct 18 18:38:21 1999 +0200
+++ b/doc-src/System/fonts.tex Mon Oct 18 19:43:18 1999 +0200
@@ -3,74 +3,68 @@
\chapter{Fonts and character encodings}
-With the advent of print modes in Isabelle, variant forms of output
-have become very easy. As the canonical application of this feature,
-{\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF) support
-optional input and output of nice mathematical symbols as built-in
-option.
+Using the print mode mechanism of Isabelle, variant forms of output become
+very easy. As the canonical application of this feature, {\Pure} and major
+object-logics (\FOL, \ZF, \HOL, \HOLCF) support optional input and output of
+proper mathematical symbols as built-in option.
-Symbolic output is enabled by activating the \ttindex{symbols} print
-mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
-\S\ref{sec:interface}) usually do this already by default.
+Symbolic output is enabled by activating the ``\ttindex{symbols}'' print mode.
+User interfaces (e.g.\ \texttt{isa-xterm}, see \S\ref{sec:interface}) usually
+do this already by default.
-\medskip Displaying non-standard characters requires special screen
-fonts, of course. The \texttt{installfonts} utility takes care of this
-(see \S\ref{sec:tool-installfonts}). Furthermore, some {\ML} systems
-disallow non-\textsc{ascii} characters in literal string constants.
-This problem is avoided by appropriate input filtering (see
-\S\ref{sec:tool-symbolinput}).
+\medskip Displaying non-standard characters requires special screen fonts. The
+\texttt{installfonts} utility takes care of this (see
+\S\ref{sec:tool-installfonts}). Furthermore, some {\ML} systems disallow
+non-\textsc{ascii} characters in literal string constants. This problem is
+avoided by appropriate input filtering (see \S\ref{sec:tool-symbolinput}).
-These things usually happen behind the scenes. Users normally do not
-have to read the explanations below, unless something really fails to
-work.
+These things usually happen behind the scenes. Users normally do not have to
+read the explanations below, unless something really fails to work.
\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
\label{sec:tool-installfonts}
-The \tooldx{installfonts} utility ensures that your currently running
-X11 display server (as determined by the \texttt{DISPLAY} environment
-variable) knows about the Isabelle fonts. Its usage is:
+The \tooldx{installfonts} utility ensures that your currently running X11
+display server (as determined by the \texttt{DISPLAY} environment variable)
+knows about the Isabelle fonts. Its usage is:
\begin{ttbox}
Usage: isatool installfonts
Install the isabelle fonts into your X11 server.
(May be safely called repeatedly.)
\end{ttbox}
-Note that this need not be called manually under normal circumstances
---- user interfaces depending on the Isabelle fonts usually invoke
+Note that this need not be called manually under normal circumstances --- user
+interfaces depending on the Isabelle fonts usually invoke
\texttt{installfonts} automatically.
-\medskip As simple as this might appear to be, it is not! X11 fonts
-are a surprisingly complicated matter. Depending on your network
-structure, fonts might have to be installed differently. This has to
-be specified via the \settdx{ISABELLE_INSTALLFONTS} variable in your
-local settings.
+\medskip As simple as this might appear to be, it is not! X11 fonts are a
+surprisingly complicated matter. Depending on your network structure, fonts
+might have to be installed differently. This has to be specified via the
+\settdx{ISABELLE_INSTALLFONTS} variable in your local settings.
-\medskip In the simplest situation, X11 is used only locally, i.e.\
-the client program (Isabelle) and the display server are run on the
-same machine. In this case, most X11 display servers should be happy
-by being told about the Isabelle fonts directory as follows:
+\medskip In the simplest situation, X11 is used only locally, i.e.\ the client
+program (Isabelle) and the display server are run on the same machine. In that
+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"%$
\end{ttbox}
-The same also works for remote X11 sessions in a somewhat homogeneous
-network, where any X11 display machine also mounts the Isabelle
-distribution under the \emph{same} name as the client side.
+The same also works for remote X11 sessions in a largely homogeneous network,
+where any X11 display machine also mounts the Isabelle distribution under the
+\emph{same} name as the client side.
-\medskip Above method fails, though, if the display machine does have
-the font files at the same location as the client. In case your server
-is a full workstation with its own file system, you could in principle
-just copy the fonts there and do an appropriate \texttt{xset~fp+}
-manually before running the Isabelle interface. This is very awkward,
-of course. It is even impossible for proper X11 terminals that do not
-have their own file system.
+\medskip Above method fails, though, if the display machine does have the font
+files at the same location as the client. In case your server is a full
+workstation with its own file system, you could in principle just copy the
+fonts there and do an appropriate \texttt{xset~fp+} manually before running
+the Isabelle interface. This is very awkward, of course. It is even impossible
+for proper X11 terminals that do not have their own file system.
-A much better solution is to have a \emph{font server} offer the
-Isabelle fonts to any X11 display on the network. There are already
-suitable servers running at Munich and Cambridge. So in case you have
-a sensible Internet connection to either site, you may just attach
-yourself as follows:
+A much better solution is to have a \emph{font server} offer the Isabelle
+fonts to any X11 display on the network. There are already suitable servers
+running at Munich and Cambridge. So in case you have a permanent Internet
+connection to either site, you may just attach yourself as follows:
\begin{ttbox}
ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
\end{ttbox}
@@ -79,59 +73,55 @@
ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"
\end{ttbox}
-\medskip In the unfortunate case that neither local fonts work, nor
-accessing our world-wide font service is practical, it might be best
-to start your own in-house font service. This is in principle easy to
-setup. The program is called \texttt{xfs} (sometimes just
-\texttt{fs)}, see the \texttt{man} pages of your system. There is an
-example fontserver configuration available in the
-\texttt{lib/fontserver} directory of the Isabelle distribution.
+\medskip In the unfortunate case that neither local fonts work, nor accessing
+our world-wide font service is practical, it might be best to start your own
+in-house font service. This is in principle quite easy to setup. The program
+is called \texttt{xfs} (sometimes just \texttt{fs)}, see the \texttt{man}
+pages of your system. There is an example fontserver configuration available
+in the \texttt{lib/fontserver} directory of the Isabelle distribution.
\section{Check for non-ASCII characters --- \texttt{isatool nonascii}}
\label{sec:tool-nonascii}
-The \tooldx{nonascii} utility checks files for non-\textsc{ascii}
-characters:
+The \tooldx{nonascii} utility checks files for non-\textsc{ascii} characters:
\begin{ttbox}
Usage: nonascii [FILES|DIRS...]
Recursively find .thy/.ML files and check for non-\textsc{ascii}
characters.
\end{ttbox}
-Under normal circumstances, non-\textsc{ascii} characters do not
-appear in theories and proof scripts.
+Under normal circumstances, non-\textsc{ascii} characters do not appear in
+theories and proof scripts.
\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
\label{sec:tool-symbolinput}
-Processing non-\textsc{ascii} text is notoriously difficult. In
-particular, some {\ML} systems reject character codes outside the
-range 32--127 as part of literal string constants. In order to
-circumvent such restrictions, Isabelle employs a general notation
-where glyphs are referred by some symbolic name instead of their
-actual encoding: The general form is \verb|\<|$charname$\verb|>|.
+Processing non-\textsc{ascii} text is notoriously difficult. In particular,
+some {\ML} systems reject character codes outside the range 32--127 as part of
+literal string constants. In order to circumvent such restrictions, Isabelle
+employs a general notation where glyphs are referred by some symbolic name
+instead of their actual encoding: the general form is
+\verb|\<|$charname$\verb|>|.
-The \tooldx{symbolinput} utility converts a input stream encoded
-according to the standard Isabelle font layout into pure
-\textsc{ascii} text. There is no usage --- \texttt{symbolinput} just
-works from standard input to standard output, without any options
-available.
+The \tooldx{symbolinput} utility converts an input stream encoded according to
+the standard Isabelle font layout into pure \textsc{ascii} text. There is no
+usage --- \texttt{symbolinput} just works from standard input to standard
+output, without any options available.
-\medskip For example, the non-\textsc{ascii} input string \texttt{"A
- $\land$ B $\lor$ C"} will be replaced by \verb|"A \\<and> B \\<or> C"|.
-Note that the \verb|\| are escaped, accomodating concrete {\ML} string
-syntax.
+\medskip For example, the non-\textsc{ascii} input string \texttt{"A $\land$ B
+ $\lor$ C"} will be replaced by \verb|"A \\<and> B \\<or> C"|. Note that the
+\verb|\| are escaped, accommodating concrete {\ML} string syntax.
-\medskip In many cases, it might be wise not to rely on symbolic
-characters and avoid non-\textsc{ascii} text in files altogether (see
-also \S\ref{sec:tool-nonascii}). Then symbolic syntax would be really
-optional, with always suitable \textsc{ascii} representations
-available: In theory definitions, symbols appear only in mixfix
-annotations --- using the \verb|\<|$charname$\verb|>| form, proof
-scripts are just left in plain \textsc{ascii}. Thus users with
-\textsc{ascii}-only facilities will still be able to read your files.
+\medskip In many cases, it might be wise not to rely on symbolic characters
+and avoid non-\textsc{ascii} text in files altogether (see also
+\S\ref{sec:tool-nonascii}). Then symbolic syntax would be really optional,
+with always suitable \textsc{ascii} representations available. In syntax
+definitions, symbols appear only in mixfix annotations (using the
+\verb|\<|$charname$\verb|>| form), while proof texts are left in plain
+\textsc{ascii}. Thus users with \textsc{ascii}-only facilities will still be
+able to read your files.
%%% Local Variables:
%%% mode: latex
--- a/doc-src/System/misc.tex Mon Oct 18 18:38:21 1999 +0200
+++ b/doc-src/System/misc.tex Mon Oct 18 19:43:18 1999 +0200
@@ -15,15 +15,14 @@
View Isabelle documentation DOC, or show list of available documents.
\end{ttbox}
-If called without arguments, it lists all available documents. Each
-line starts with an identifier, followed by some comment. Any of these
-identifiers may be specified as the first argument in order to have
-the corresponding document displayed.
+If called without arguments, it lists all available documents. Each line
+starts with an identifier, followed by a short description. Any of these
+identifiers may be specified as the first argument in order to have the
+corresponding document displayed.
-\medskip The \texttt{ISABELLE_DOCS} setting specifies the list of
-directories (separated by colons) to be scanned for documentations.
-The program for viewing \texttt{dvi} files is determined by the
-\texttt{DVI_VIEWER} setting.
+\medskip The \texttt{ISABELLE_DOCS} setting specifies the list of directories
+(separated by colons) to be scanned for documentations. The program for
+viewing \texttt{dvi} files is determined by the \texttt{DVI_VIEWER} setting.
\section{Tuning proof scripts --- \texttt{isatool expandshort}}
@@ -40,17 +39,16 @@
Renames old versions of files by appending "~~".
\end{ttbox}
-In the files or directories supplied as arguments, all occurrences of
-the shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts
-are replaced with the corresponding full commands. The old versions
-of the files are renamed to have the suffix~\verb'~~'.
+In the files or directories supplied as arguments, all occurrences of the
+shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts are
+replaced with the corresponding full commands. The old versions of the files
+are renamed to have the suffix``~\verb'~~'''.
\section{Getting logic images --- \texttt{isatool findlogics}}
The \tooldx{findlogics} utility traverses all directories specified in
-\texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage
-is:
+\texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage is:
\begin{ttbox}
Usage: isatool findlogics
@@ -65,9 +63,9 @@
\section{Inspecting the settings environment -- \texttt{isatool getenv}}
\label{sec:tool-getenv}
-The Isabelle settings environment --- as provided by the site-default
-and user-specific settings files --- can be inspected with the
-\tooldx{getenv} utility:
+The Isabelle settings environment --- as provided by the site-default and
+user-specific settings files --- can be inspected with the \tooldx{getenv}
+utility:
\begin{ttbox}
Usage: isatool getenv [OPTIONS] [VARNAMES ...]
@@ -78,26 +76,25 @@
Get value of VARNAMES from the Isabelle settings.
\end{ttbox}
-With the \texttt{-a} option, one may inspect the full process
-environment that Isabelle related programs are run in. This usually
-contains much more variables than are actually Isabelle settings.
-Normally, output is a list of lines of the form
-\mbox{$name$\texttt{=}$value$}. The \texttt{-b} option causes only the
-values to be printed.
+With the \texttt{-a} option, one may inspect the full process environment that
+Isabelle related programs are run in. This usually contains much more
+variables than are actually Isabelle settings. Normally, output is a list of
+lines of the form \mbox{$name$\texttt{=}$value$}. The \texttt{-b} option
+causes only the values to be printed.
\subsection*{Examples}
-Get the {\ML} system identifier and the location where the compiler
-binaries are supposed to reside as follows:
+Get the {\ML} system identifier and the location where the compiler binaries
+are supposed to reside as follows:
\begin{ttbox}
isatool getenv ML_SYSTEM ML_HOME
{\out ML_SYSTEM=smlnj-110}
{\out ML_HOME=/usr/local/smlnj-110/bin}
\end{ttbox}
-The next one peeks at the search path that \texttt{isabelle} uses to
-locate logic images:
+The next one peeks at the search path that \texttt{isabelle} uses to locate
+logic images:
\begin{ttbox}
isatool getenv -b ISABELLE_PATH
{\out /home/me/isabelle/heaps/smlnj-110:/usr/local/isabelle/heaps/smlnj-110}
@@ -108,15 +105,16 @@
\begin{ttbox}
ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps
\end{ttbox}
-Note how the \texttt{ML_SYSTEM} value got appended automatically to
-each path component. This is a special feature of
-\texttt{ISABELLE_PATH} (and also of \texttt{ISABELLE_OUTPUT}).
+Note how the \texttt{ML_SYSTEM} value got appended automatically to each path
+component. This is a special feature of \texttt{ISABELLE_PATH} (and also of
+\texttt{ISABELLE_OUTPUT}).
\section{Installing standalone Isabelle executables -- \texttt{isatool install}}
+\label{sec:tool-install}
-Usually, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool} etc.) are
-just run from their location within the distribution directory, probably
+By default, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool} etc.)
+are just run from their location within the distribution directory, probably
indirectly by the shell through its \texttt{PATH}. Other schemes of
installation are supported by the \tooldx{install} utility:
\begin{ttbox}
@@ -142,8 +140,9 @@
note that a plain manual copy of the original Isabelle executables just would
not work!
-The \texttt{-k} option creates an Isabelle application object for the K
-desktop environment. The icon will appear directly on Desktop.
+The \texttt{-k} option creates an Isabelle application object for the popular
+\textsl{K~Desktop Environment} (KDE)\index{KDE}. The icon will appear
+directly on Desktop.
\section{Creating instances of the Isabelle logo -- \texttt{isatool
--- a/doc-src/System/present.tex Mon Oct 18 18:38:21 1999 +0200
+++ b/doc-src/System/present.tex Mon Oct 18 19:43:18 1999 +0200
@@ -6,10 +6,10 @@
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.
+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 leave
+positions. 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.
@@ -23,8 +23,8 @@
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.
+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
@@ -35,10 +35,9 @@
\medskip
-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
+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
\begin{ttbox}
ISABELLE_USEDIR_OPTIONS="-i true"
@@ -47,8 +46,8 @@
distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
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.\
+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}
@@ -72,8 +71,8 @@
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}. Section headings may be included
-in the presentation via the {\ML} function
+\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}
@@ -101,12 +100,11 @@
\section{Browsing theory graphs} \label{sec:browse}
\index{theory graph browser|bold}
-The graph browser is a tool for visualizing dependency graphs of
-Isabelle theories. 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 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.
\subsection{Invoking the graph browser}
@@ -121,8 +119,8 @@
\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
+Web browser and selecting the version ``including theory graph browser''.
+There is also a link to the corresponding theory graph in every logic's {\tt
index.html} file.
@@ -140,8 +138,8 @@
\subsubsection*{The directory tree window}
-This section describes the usage of the directory browser and the
-meaning of the different items in the browser window.
+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
@@ -157,10 +155,10 @@
also be unfolded by clicking on the corresponding node in the right
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
- corresponding node. Double clicking invokes a text viewer window in
- which the contents of the theory file are displayed.
+\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}
@@ -186,7 +184,7 @@
follows:
\begin{description}
-\item[Open$\ldots$] Open a new graph file.
+\item[Open \dots] Open a new graph file.
\item[Export to PostScript] Outputs the current graph in {\sc
PostScript} format, appropriately scaled to fit on one single
@@ -239,7 +237,7 @@
\label{sec:tool-document}
The \tooldx{document} utility prepares logic session documents, processing the
-sources both provided by the user and generated by Isabelle. Its usage is:
+sources both as provided by the user and generated by Isabelle. Its usage is:
\begin{ttbox}
Usage: document [OPTIONS] [DIR]
@@ -251,14 +249,14 @@
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.
+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 actual document, apart from the
-actual theories as generated by Isabelle.
+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
@@ -284,9 +282,9 @@
\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.}
+{\TeX} inputs path. For proper setup of PDF documents (with hyperlinks,
+bookmarks, and thumbnail images), 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
@@ -314,7 +312,7 @@
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.).
+(\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
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
@@ -354,14 +352,13 @@
\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.
+browsing information and document preparation is controlled here.
\subsection*{Options}
-Basically, there are two different modes of operation: \emph{build
- mode} (enabled through the \texttt{-b} option) and \emph{example
- mode} (default).
+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
@@ -374,34 +371,32 @@
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.
+and automatically runs \texttt{ROOT.ML} from within directory \texttt{NAME}.
+It assumes that this file 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{-i} option controls theory browser data generation. It
+may be explicitly turned on or off --- as usual, 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},
+arguments are \texttt{false} (do not prepare any 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}.
+ 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 in turn 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.
+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 explicitly via the \texttt{-s} option.
\subsection*{Examples}
--- a/doc-src/System/system.tex Mon Oct 18 18:38:21 1999 +0200
+++ b/doc-src/System/system.tex Mon Oct 18 19:43:18 1999 +0200
@@ -27,8 +27,8 @@
\include{basics}
\include{present}
+\include{misc}
\include{fonts}
-\include{misc}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing