--- a/doc-src/System/basics.tex Fri May 16 15:55:02 1997 +0200
+++ b/doc-src/System/basics.tex Fri May 16 15:57:11 1997 +0200
@@ -5,28 +5,28 @@
The \emph{Isabelle System Manual} describes Isabelle together with its
related tools and user interfaces --- as seen from an outside
-(operating system oriented) view. On the other hand, see
-\emph{Isabelle Reference} for all internal {\ML} level user commands.
+(operating system oriented) view. See the \emph{Isabelle Reference
+ Manual} for all internal {\ML} level user commands, on the other
+hand.
\medskip The Isabelle system level environment is based on a few
-generic concepts that are simple, but non-trivial:
+general concepts:
\begin{itemize}
\item The \emph{Isabelle settings mechanism}, which provides
- environment values to all Isabelle programs (including tools and
+ environment variables to all Isabelle programs (including tools and
user interfaces).
\item \emph{Isabelle proper} (\ttindex{isabelle}), which runs 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 miscellaneous utilities.
+ 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
- (this may include third-party ones).
+ provides some abstraction over the actual user interface to be used.
\end{itemize}
\medskip The beginning user would probably just run one of the
@@ -64,27 +64,27 @@
\subsection{Building the environment}
-The environment that all Isabelle programs are run in is built as
-follows:
+Whenever any of the Isabelle executables is run, theri settings
+environment is built as follows:
\begin{enumerate}
-\item The special variable \ttindex{ISABELLE_HOME} is determined
- automatically from the location of the binary that has been run
- (e.g.\ \texttt{isabelle}).
+\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 GNU
- bash script with the variable auto-export option enabled.
+\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a
+ shell script with the auto-export option for variables enabled.
- The file typically contains a rather long list of assigments
- \texttt{FOO="bar"}, thus providing the site default settings. The
- Isabelle distribution already contains a global settings file with
- sensible defaults. When installing the system, only a few of these
- have to be adapted (most likely \texttt{ML_SYSTEM} and friends).
+ This file typically contains a rather long list of assigments
+ \texttt{FOO="bar"}, 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. The
@@ -96,52 +96,119 @@
Typically, user settings are a few lines only, just containing the
assigments that are really required. One should definitely
\emph{not} start with a full copy the central
- \texttt{\$ISABELLE_HOME/etc/settings}. This may cause severe
+ \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very anoying
maintainance problems later, when the Isabelle installation is
updated or changed otherwise.
\end{enumerate}
-Note that settings files are actually bash scripts. So one may use
-complex shell commands, e.g.\ \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.
+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.
-\medskip A few variables are somewhat:
+\medskip A few variables are somewhat special:
\begin{itemize}
-\item \ttindex{ISABELLE} and \ttindex{ISATOOL} are set automatically
- to the absolute path names of the \texttt{isabelle} and
+\item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to
+ the absolute path names of the \texttt{isabelle} and
\texttt{isatool} executables, respectively.
-\item \ttindex{ISABELLE_PATH} and \ttindex{ISABELLE_OUTPUT} will have
+\item \settdx{ISABELLE_PATH} and \settdx{ISABELLE_OUTPUT} will have
the {\ML} system identifier (as specified by \texttt{ML_SYSTEM})
automatically appended to their values.
\end{itemize}
\medskip The Isabelle settings scheme is basically quite simple, but
non-trivial. For debugging purposes, the generated environment may be
-inspected with the \texttt{getenv} Isabelle tool, see
+inspected with the \texttt{getenv} utility, see
\S\ref{sec:tool-getenv}.
\subsection{Common variables}
-Below is a reference of common Isabelle settings variables. The list
-is somewhat open-ended, in particular, third-party utilities or
-interfaces may add their own selection.
+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 *.
+
+\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_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.
-\begin{ttdescription}
-\item[FIXME] FIXME
-\end{ttdescription}
+\item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS}]
+ 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.
+
+\item[\settdx{ISABELLE_PATH}*] is a list of directories (separated by
+ colons) where Isabelle logic images may reside. Note that the
+ \texttt{ML_SYSTEM} identifier is appended to each component
+ automatically.
+
+\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
+ files should be stored. The \texttt{ML_SYSTEM} identifier is
+ appended here, too.
+
+\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 implicitely 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_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 program 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 running X11 display
+ server. X11 fonts are a non-trivial issue, see \S\ref{sec:fonts} for
+ more information.
+
+\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.
+
+\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. The usage is:
+underlying {\ML} system, and over the actual heap file locations. Its
+usage is:
\begin{ttbox}
Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
@@ -158,72 +225,89 @@
\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 the given order.
-Short output names are relative to the directory specified by
+components separated by colons --- these are tried in order. Short
+output names are relative to the directory specified by
\texttt{ISABELLE_OUTPUT} setting. In any case, actual file locations
-can be given by including at least one \texttt{/} (use \texttt{./} to
-refer to the current directory).
-
-If the input heap file is not writable, or the \texttt{-r} option is
-given explicitely, the session will be read-only. That is, the {\ML}
-world cannot be committed back into the logic image. A writable
-session enables commits into either the input file, or into an
-alternative output heap file which may be given as the second
-argument.
-
-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 no longer needed heap files.
+could also be given by including at least one \texttt{/} in the name
+(use \texttt{./} to refer to the current directory).
\subsection*{Options}
-Using \texttt{-e} one may pass {\ML} code to the Isabelle session from
-the command line. Multiple \texttt{-e}'s are evaluated in the given
-order.
+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).
+
+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 \texttt{-m} option addes print mode identifiers to be made active
-for this session. Typically this is used by some user interface to
-enable output of mathematical symbols from a special screen font, for
-example (see also \S\ref{sec:fonts} about fonts and the \emph{Isabelle
- Reference Manual} about print modes in general).
+\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 supplied. Also make sure that
+commands are terminated properly by semicolon.
-Isabelle normally enters an interactice {\ML} top-level loop (after
-processing the \texttt{-e} texts). The \texttt{-q} option inhibits
-this, providing a pure batch mode facility.
+\medskip The \texttt{-m} option adds identifiers of print modes that
+are 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. See also \S\ref{sec:tool-installfonts}
+about fonts and the \emph{Isabelle Reference Manual} about print modes
+in general.
+
+\medskip Isabelle normally enters an interactice {\ML} top-level loop
+(after processing the \texttt{-e} texts). The \texttt{-q} option
+inhibits this, thus providing a pure batch mode facility.
\subsection*{Examples}
-Run an interactive session of the default object-logic:
+Run an interactive session of the default object-logic (as specified
+by the \texttt{ISABELLE_LOGIC} setting) like this:
\begin{ttbox}
isabelle
\end{ttbox}
-Usually, this refers to one of the standard logic images, which are
-read-only by default.
-
-Run a writable session, based on \texttt{FOL}, but output to
-\texttt{Foo} (in the directory specified by the
-\texttt{ISABELLE_OUTPUT} setting):
+Usually \texttt{ISABELLE_LOGIC} refers to one of the standard logic
+images, which are read-only by default. A writable session --- based
+on \texttt{FOL}, but output to \texttt{Foo} (in the directory
+specified by the \texttt{ISABELLE_OUTPUT} setting) --- may be invoked
+as follows:
\begin{ttbox}
isabelle FOL Foo
\end{ttbox}
-Ending this session normally (e.g.\ by typing control-D), dumps the
+Ending this session normally (e.g.\ by typing control-D) dumps the
whole {\ML} system state into \texttt{Foo}. Be prepared for several
megabytes!
-The \texttt{Foo} session may be continued (writably!) at exactly the
-same point as follows:
+The \texttt{Foo} session may be continued later (still in writable
+state) at exactly the same point:
\begin{ttbox}
isabelle Foo
\end{ttbox}
+A read-only \texttt{Foo} session may be started by:
+\begin{ttbox}
+isabelle -r Foo
+\end{ttbox}
+One may also use something like \texttt{chmod~-w} on the logic image
+to have them read-only automatically.
-\medskip This is a simple batch mode example, printing a certain
-theorem of \texttt{FOL}:
+\medskip The next example demonstrates batch execution of Isabelle. We
+print a certain theorem of \texttt{FOL}:
\begin{ttbox}
isabelle -e "prth allE;" -q -r FOL
\end{ttbox}
-Note that the output text will be usually interspered with some
+Note that the output text will be usually interspersed with some
garbage produced by the {\ML} compiler.
+
+\section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool}
+
+FIXME
+
+\section{The Isabelle interface wrapper --- \texttt{Isabelle}} \label{sec:interface}
+
+FIXME
--- a/doc-src/System/fonts.tex Fri May 16 15:55:02 1997 +0200
+++ b/doc-src/System/fonts.tex Fri May 16 15:57:11 1997 +0200
@@ -1,17 +1,86 @@
\chapter{Fonts and character encodings}
-\section{ --- \texttt{isatool installfonts}}
+With the advent of print modes in Isabelle (see also The
+\emph{Isabelle Reference Manual}, 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 output
+(and input) of nice mathematical symbols out of the box.
+
+Symbolic output is enabled by activating the \ttindex{symbols} print
+mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
+\S\ref{sec:isa-xterm}) usually do this by default.
+\medskip Of course, this requires special screen fonts (see
+\S\ref{sec:tool-installfonts}). Furthermore, various {\ML} systems
+cause some problems with non-\textsc{ascii} characters in literal
+strings. These are avoided by the \texttt{symbolinput} filter (see
+\S\ref{sec:tool-symbolinput}).
+
+Both of these are invoked transparently in normal operation. So one
+does not actually have to read the explanations below, unless
+something fails to work.
+
+
+\section{Telling X11 about 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:
\begin{ttbox}
Usage: isatool installfonts
Install the isabelle fonts into your X11 server.
- (May be savely called repeatedly.)
+ (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 will invoke
+\texttt{installfonts} transparently.
+
+\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}.
+
+\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. Then most X11 display servers should be happy to being
+just told about the directory where the fonts reside within the
+Isabelle distribution:
+\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 the X11 display machine mounts the Isabelle
+distribution under the same name as the client side.
+
+\medskip Above method fails, 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 awkward, of course, but
+is even \emph{impossible} for proper X terminals that do not have
+their own file system.
+
+A much better solution to this problem is to use an \emph{X11 font
+ server}, offering the Isabelle font to the Net. In principle it is
+relatively easy to setup one your own --- the program is called
+\texttt{xfs} (or just \texttt{fs)}, see the \texttt{man} pages of your
+system.
+
+Your are very lucky, though, if you have a sensible connection to the
+Internet. We already offer a world-wide X11 font service for the
+Isabelle fonts. To have \texttt{installfonts} make use of this, just
+set \texttt{ISABELLE_INSTALLFONTS} is follows:
+\begin{ttbox}
+ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
\end{ttbox}
-\section{ --- \texttt{isatool symbolinput}}
+
+\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
+\label{sec:tool-symbolinput}
%FIXME not yet
--- a/doc-src/System/misc.tex Fri May 16 15:55:02 1997 +0200
+++ b/doc-src/System/misc.tex Fri May 16 15:57:11 1997 +0200
@@ -3,6 +3,64 @@
\chapter{Miscellaneous tools}
+Subsequently we describe various Isabelle related utilities --- in
+alphabetical order.
+
+
+\section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc}
+
+The \tooldx{doc} utility displays online documentation:
+\begin{ttbox}
+Usage: isatool doc [DOC]
+
+ 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.
+
+\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 set in
+\texttt{DVI_VIEWER}.
+
+
+\section{Tuning proof scripts --- \texttt{isatool expandshort}}
+
+The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance
+readability a bit:
+\begin{ttbox}
+Usage: expandshort [FILES ...]
+
+ Expand shorthand goal commands in FILES. Also contracts uses of
+ resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on
+ 1-element lists; furthermore expands tabs, since they are now
+ forbidden in ML string constants.
+
+ Renames old versions of FILES by appending "~~".
+\end{ttbox}
+In the files supplied as arguments, all occurrences of the shorthand
+commands \texttt{br}, \texttt{be} etc.\ are replaced with the
+corresponding full commands. Shorthand commands should appear one per
+line. The old versions of the files are renamed to have the
+suffix~\verb'~~'.
+
+\section{Get 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:
+\begin{ttbox}
+Usage: isatool findlogics
+
+ Collect heap file names from ISABELLE_PATH.
+\end{ttbox}
+The base names of all files found on the path are printed --- sorted
+and with duplicates removed. Also note that \texttt{ISABELLE_PATH}
+implicitely depends upon \texttt{ML_SYSTEM}. Thus switching to another
+{\ML} compiler may change the set of logic images available.
+
\section{Inspecting the settings environment -- \texttt{isatool getenv}}
\label{sec:tool-getenv}
@@ -23,26 +81,26 @@
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.
-
-Unless the \texttt{-b} option is given, the output is a list of lines
-of the form $varname\mathtt{=}value$.
+Normally output is a list of lines of the form
+\mbox{$varname$\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 be installed as follows:
+binaries are supposed to reside as follows:
\begin{ttbox}
isatool getenv ML_SYSTEM ML_HOME
+{\out ML_SYSTEM=smlnj-1.09}
{\out ML_HOME=/usr/local/sml109.27/bin}
-{\out ML_SYSTEM=smlnj-1.09}
\end{ttbox}
-This one peeks at the search path that \texttt{isabelle} uses to
+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/mmw/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09}
+{\out /home/me/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09}
\end{ttbox}
We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=}
prefix. The value above is what became of the following assignment in
@@ -50,36 +108,41 @@
\begin{ttbox}
ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps
\end{ttbox}
-Note how \texttt{\$ML_SYSTEM} got appended automatically to each path
-component. This is a special feature of \texttt{ISABELLE_PATH} (and
-also of \texttt{ISABELLE_OUTPUT}).
-
-\section{Get logic images --- \texttt{isatool findlogics}}
+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}).
-\begin{ttbox}
-Usage: isatool findlogics
-
- Collect heap file names from ISABELLE_PATH.
-\end{ttbox}
\section{Isabelle's version of make --- \texttt{isatool make}}
+The Isabelle \tooldx{make} utility is a very simple wrapper for
+ordinary Unix \texttt{make}:
\begin{ttbox}
Usage: isatool make [ARGS ...]
Compiles logic in current directory using IsaMakefile.
ARGS are directly passed to the system make program.
\end{ttbox}
+Note that the Isabelle settings environment is also active. Thus one
+may refer to its values within the \texttt{IsaMakefile}, e.g.\
+\texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the
+make file also inherit this environment.
+
+\medskip You may want to have a look at the \texttt{IsaMakefile}s of
+the distributed object-logics as examples for your own developements.
-\section{ --- \texttt{isatool usedir}}
+\section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir}
+FIXME
+
+%FIXME
+% -g BOOL generate theory graph data (default false)
\begin{ttbox}
Usage: isatool usedir LOGIC NAME
Options are:
-b build mode (output heap image, use dir ".")
- -g BOOL generate theory graph data (default false)
-h BOOL generate theory HTML data (default false)
-s NAME override session NAME
@@ -87,25 +150,4 @@
information (HTML etc.) according to settings.
\end{ttbox}
-
-\section{ --- \texttt{isatool doc}}
-
-\begin{ttbox}
-Usage: isatool doc [DOC]
-
- View Isabelle documentation DOC, or show list of available documents.
-\end{ttbox}
-
-
-\section{ --- \texttt{isatool expandshort}}
-
-\begin{ttbox}
-Usage: expandshort [FILES ...]
-
- Expand shorthand goal commands in FILES. Also contracts uses of
- resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on
- 1-element lists; furthermore expands tabs, since they are now
- forbidden in ML string constants.
-
- Renames old versions of FILES by appending "~~".
-\end{ttbox}
+FIXME
--- a/doc-src/System/present.tex Fri May 16 15:55:02 1997 +0200
+++ b/doc-src/System/present.tex Fri May 16 15:57:11 1997 +0200
@@ -6,10 +6,10 @@
Isabelle is able to make HTML documents that show a theory's
definition, the theorems proved in its ML file and the relationship
-with its ancestors and descendants. HTML stands for Hypertext Markup
-Language and is used in the World Wide Web to represent text
-containing images and links to other documents. Web browsers like
-{\tt xmosaic} or {\tt netscape} are used to view these documents.
+with its ancestors and descendants. HTML is the hypertext markup
+language used on the World Wide Web to represent text containing
+images and links to other documents. These documents may be viewed
+using Web browsers like Netscape or Lynx.
Besides the three HTML files that are made for every theory
(definition and theorems, ancestors, descendants), Isabelle stores
@@ -17,62 +17,39 @@
linked with other indexes to represent the hierarchic structure of
Isabelle's logics.
-To make HTML files for logics that are part of the Isabelle
-distribution, simply set the shell environment variable {\tt
-MAKE_HTML} before compiling a logic. This works for single logics as
-well as for the shell script {\tt make-all} (see
-\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
-{\tt csh} style shell, the following commands can be used:
-
+\medskip To make HTML files for logics that are part of the Isabelle
+distribution, simply append ``\texttt{-h true}'' to the
+\texttt{ISABELLE_USEDIR_OPTIONS} setting before making a logic. For
+example, to generate HTML files for {\FOL}, first add something like
+this to your \texttt{\~\relax/isabelle/etc/settings} file:
\begin{ttbox}
-cd FOL
-setenv MAKE_HTML
-make
+ISABELLE_USEDIR_OPTIONS="-h true"
\end{ttbox}
-
-The databases made this way do not differ from the ones made with an
-unset {\tt MAKE_HTML}; in particular no HTML files are written if the
-database is used to manually load a theory.
+Then \texttt{cd} into the \texttt{src/FOL} directory of the Isabelle
+distribution and do an \texttt{isatool make} (or even \texttt{isatool
+ make test}).
-As you will see below, the HTML generation is controlled by a boolean
-reference variable. If you want to make databases which define this
-variable's value as {\tt true} and where therefore HTML files are
-written each time {\tt use_thy} is invoked, you have to set {\tt
-MAKE_HTML} to ``{\tt true}'':
-
-\begin{ttbox}
-cd FOL
-setenv MAKE_HTML true
-make
-\end{ttbox}
-
-All theories loaded from within the {\tt FOL} database and all
-databases derived from it will now cause HTML files to be written.
-This behaviour can be changed by assigning a value of {\tt false} to
-the boolean reference variable {\tt make_html}. Be careful when making
-such databases publicly available since it means that your users will
-generate HTML files though they might not intend to do so.
-
-As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
-{\tt FOL}) and because the HTML files list a theory's ancestors, you
-should not make HTML files for a logic if the HTML files for the base
-logic do not exist. Otherwise some of the hypertext links might point
-to non-existing documents.
+\medskip As some of Isabelle's logics are based on others (e.g. {\tt
+ ZF} on {\tt FOL}) and because the HTML files list a theory's
+ancestors, you should not make HTML files for a logic if the HTML
+files for the base logic do not exist. Otherwise some of the hypertext
+links might point to non-existing documents.
The entry point to all logics is the {\tt index.html} file located in
-Isabelle's main directory. You can also access a HTML version of the
-distribution package at
+Isabelle's main directory.
+A complete HTML version of all distributed Isabelle object-logics and
+examples may be accessed on the WWW at:
\begin{ttbox}
http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
\end{ttbox}
+Note that this is not necessarily consistent with your local sources!
-\section*{Manual HTML generation}
+\section*{*HTML generation internals}
-To manually control the generation of HTML files the following
-commands and reference variables are used:
-
+The generation of HTML files is controlled by the following {\ML}
+commands and reference variables:
\begin{ttbox}
init_html : unit -> unit
make_html : bool ref
@@ -98,10 +75,10 @@
{\tt init_html} and makes the {\tt index.html} file. If {\tt
make_html} is {\tt false} nothing is done.
-The indexes made by this function also contain a link to the {\tt
-README} file if there exists one in the directory where the index is
-stored. If there's a {\tt README.html} file it is used instead of
-{\tt README}.
+The indexes made by this function also contain a link to the
+\texttt{README.html} or \texttt{README} file if there exists one in
+the directory where the index is stored. If there's a {\tt
+ README.html} file it is used instead of {\tt README}.
\end{ttdescription}
@@ -109,24 +86,24 @@
\begin{ttbox}
init_html();
-{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
+{\out Setting path for index.html to "/home/me/Isabelle-dist/src/HOL"}
use_thy "List";
\dots
finish_html();
\end{ttbox}
Please note that HTML files are made only for those theories that are
-read while {\tt make_html} is {\tt true}. These files may contain
-links to theories that were read with a {\tt false} {\tt make_html}
-and therefore point to non-existing files.
+read while \texttt{make_html} is \texttt{true}. These files may
+contain links to theories that were read with a \texttt{make_html} set
+to \texttt{false} and therefore point to non-existing files.
\section*{Extending or adding a logic}
-If you add a new subdirectory to Isabelle's logics (or add a completly
-new logic), you would have to call {\tt init_html} at the start of every
-directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
-it. This is automatically done if you use
+If you add a new subdirectory to Isabelle's logics (or add a
+completely new logic), you would have to call {\tt init_html} at the
+start of every directory's {\tt ROOT.ML} file and {\tt finish_html} at
+the end of it. This is automatically done if you use
\begin{ttbox}\index{*use_dir}
use_dir : string -> unit
@@ -137,31 +114,15 @@
executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
index.html} file written in this directory will be automatically
linked to the first index found in the (recursively searched)
-superdirectories.
-
-Instead of adding something like
+super directories.
-\begin{ttbox}
-use"ex/ROOT.ML";
-\end{ttbox}
-
-to the logic's makefile you have to use this:
+The \texttt{usedir} utility (see also \S\ref{sec:tool-usedir}) will
+automatically take care of this.
-\begin{ttbox}
-use_dir"ex";
-\end{ttbox}
-
-Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
-{\tt true} the generation of HTML files depends on the value this
-reference variable has. It can either be inherited from the used \ML{}
-database or set in the makefile before {\tt use_dir} is invoked,
-e.g. to set it's value according to the environment variable {\tt
-MAKE_HTML}.
-
-The generated HTML files contain all theorems that were proved in the
-theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
-or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
-is a hypertext link to the whole \ML{} file.
+\medskip The generated HTML files contain all theorems that were
+proved in the theory's \ML{} file with {\tt qed}, {\tt qed_goal} and
+{\tt qed_goalw}, or stored with {\tt bind_thm} and {\tt store_thm}.
+Additionally, there is a hypertext link to the whole \ML{} file.
You can add section headings to the list of theorems by using
@@ -171,11 +132,10 @@
in a theory's ML file, which converts a plain string to a HTML
heading and inserts it before the next theorem proved or stored with
-one of the above functions. If {\tt make_html} is {\tt false} nothing
-is done.
+one of the above functions.
-\section*{Using someone else's database}
+\section*{*Using someone else's database}
To make them independent from their storage place, the HTML files only
contain relative paths which are derived from absolute ones like the
@@ -195,8 +155,8 @@
some hypertext links.
It's also a good idea to set {\tt gif_path} which points to the
-directory containing two GIF images used in the HTML
-documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
+directory containing two GIF images used in the HTML documents.
+Normally this is the \texttt{src/Tools} subdirectory of Isabelle's
main directory. While its value in general is still valid, your HTML
files would depend on files not owned by you. This prevents you from
changing the location of the HTML files (as they contain relative
@@ -207,8 +167,8 @@
someone else's \ML{} database:
\begin{ttbox}
-base_path := "/home/smith/isabelle";
-gif_path := "/home/smith/isabelle/Tools";
+base_path := "/home/someone/Isabelle-dist/src";
+gif_path := "/home/someone/Isabelle-dist/src/Tools";
init_html();
\dots
\end{ttbox}
--- a/doc-src/System/system.ind Fri May 16 15:55:02 1997 +0200
+++ b/doc-src/System/system.ind Fri May 16 15:57:11 1997 +0200
@@ -1,42 +1,62 @@
\begin{theindex}
- \item browser, \bold{13}
+ \item {\tt doc} tool, 7
+ \item {\tt DVI_VIEWER} setting, 4
\indexspace
- \item {\tt finish_html}, \bold{10}
+ \item {\tt expandshort} tool, 7
\indexspace
- \item {\tt getenv} tool, 5
+ \item {\tt findlogics} tool, 8
+ \item {\tt finish_html}, \bold{13}
+
+ \indexspace
+
+ \item {\tt getenv} tool, 8
\indexspace
- \item HTML, \bold{9}
+ \item HTML, \bold{12}
\indexspace
- \item {\tt init_html}, \bold{10}
+ \item {\tt init_html}, \bold{13}
\item {\tt INSTALL}, 1
- \item {\tt ISABELLE}, 3
+ \item {\tt installfonts} tool, 10
+ \item {\tt ISABELLE} setting, 3
\item {\tt Isabelle}, 1
- \item {\tt isabelle}, 1, 3
- \item {\tt ISABELLE_HOME}, 2
- \item {\tt ISABELLE_OUTPUT}, 3
- \item {\tt ISABELLE_PATH}, 3
- \item {\tt ISATOOL}, 3
+ \item {\tt isabelle}, 1, 4
+ \item {\tt ISABELLE_DOCS} setting, 4
+ \item {\tt ISABELLE_HOME} setting, 2, 3
+ \item {\tt ISABELLE_HOME_USER} setting, 3
+ \item {\tt ISABELLE_INSTALL_FONTS} setting, 4
+ \item {\tt ISABELLE_INSTALLFONTS} setting, 10
+ \item {\tt ISABELLE_INTERFACE} setting, 4
+ \item {\tt ISABELLE_LOGIC} setting, 4
+ \item {\tt ISABELLE_OUTPUT} setting, 3, 4
+ \item {\tt ISABELLE_PATH} setting, 3
+ \item {\tt ISABELLE_TOOLS} setting, 4
+ \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4
+ \item {\tt ISATOOL} setting, 3
\item {\tt isatool}, 1
\indexspace
- \item {\tt make_html}, \bold{10}
+ \item {\tt make} tool, 9
+ \item {\tt make_html}, \bold{13}
+ \item {\tt ML_HOME} setting, 3
+ \item {\tt ML_OPTIONS} setting, 3
+ \item {\tt ML_SYSTEM} setting, 3
\indexspace
\item settings, \bold{1}
+ \item {\tt symbols}, 10
\indexspace
- \item {\tt use_dir}, 11
+ \item {\tt use_dir}, 13, 14
\end{theindex}
--- a/doc-src/System/system.tex Fri May 16 15:55:02 1997 +0200
+++ b/doc-src/System/system.tex Fri May 16 15:57:11 1997 +0200
@@ -15,7 +15,7 @@
Computer Laboratory \\ University of Cambridge \\
\texttt{lcp@cl.cam.ac.uk}\\[3ex]
With Contributions by Tobias Nipkow and Markus Wenzel%
- \thanks{Chapter~\protect\ref{html} was written by Carsten
+ \thanks{Section~\protect\ref{sec:html} was written by Carsten
Clasohm. Chapter~\protect\ref{browse} was written by Stefan
Berghofer. Other parts are by Markus Wenzel.}}
@@ -39,7 +39,7 @@
\include{misc}
\include{fonts}
\include{present}
-\include{browse}
+%\include{browse}
%\begingroup
% \bibliographystyle{plain} \small\raggedright\frenchspacing