1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/System/basics.tex Wed May 14 19:27:21 1997 +0200
1.3 @@ -0,0 +1,229 @@
1.4 +
1.5 +% $Id$
1.6 +
1.7 +\chapter{Basic concepts}
1.8 +
1.9 +The \emph{Isabelle System Manual} describes Isabelle together with its
1.10 +related tools and user interfaces --- as seen from an outside
1.11 +(operating system oriented) view. On the other hand, see
1.12 +\emph{Isabelle Reference} for all internal {\ML} level user commands.
1.13 +
1.14 +\medskip The Isabelle system level environment is based on a few
1.15 +generic concepts that are simple, but non-trivial:
1.16 +\begin{itemize}
1.17 +\item The \emph{Isabelle settings mechanism}, which provides
1.18 + environment values to all Isabelle programs (including tools and
1.19 + user interfaces).
1.20 +\item \emph{Isabelle proper} (\ttindex{isabelle}), which runs logic
1.21 + sessions, both interactively or in batch mode. In particular,
1.22 + \texttt{isabelle} abstracts over the invocation of the actual {\ML}
1.23 + system to be used.
1.24 +\item The \emph{Isabelle tools wrapper} (\ttindex{isatool}), which
1.25 + provides a generic startup platform for miscellaneous utilities.
1.26 + Thus tools automatically benefit from the settings mechanism.
1.27 + Furthermore, the shell's search path is kept clean from many small
1.28 + programs.
1.29 +\item The \emph{Isabelle interface wrapper}
1.30 + (\ttindex{Isabelle}\footnote{Note the capital \texttt{I}!}), which
1.31 + provides some abstraction over the actual user interface to be used
1.32 + (this may include third-party ones).
1.33 +\end{itemize}
1.34 +
1.35 +\medskip The beginning user would probably just run one of the
1.36 +interfaces (by invoking the capital \texttt{Isabelle}), and maybe some
1.37 +basic other tools like \texttt{doc} (see \S\ref{sec:tool-doc}). This
1.38 +assumes that the system has already been installed properly, of
1.39 +course.\footnote{In case you have to do this yourself from scratch,
1.40 + see the \ttindex{INSTALL} file in the top-level directory of the
1.41 + distribution. The information provided there should be sufficient as
1.42 + a start.}
1.43 +
1.44 +
1.45 +\section{Isabelle settings} \label{sec:settings}
1.46 +
1.47 +The Isabelle system heavily depends on the \emph{settings
1.48 + mechanism}\indexbold{settings}. Basically, this is just a collection
1.49 +of environment variables, e.g.\ \texttt{ISABELLE_HOME},
1.50 +\texttt{ML_SYSTEM}, \texttt{ML_HOME}. These variables are \emph{not}
1.51 +intended to be set directly from the shell!
1.52 +
1.53 +Isabelle employs a somewhat more sophisticated scheme of
1.54 +\emph{settings files} --- one for site-wide defaults, another for
1.55 +optional user-specific modifications. With all configuration
1.56 +variables in only one or two places, this is considered much more
1.57 +maintainable and user-friendly than ordinary shell environment
1.58 +variables.
1.59 +
1.60 +In particular, we avoid the typical situation where prospective users
1.61 +of a software package are told to put this and that in their shell
1.62 +startup scripts. Isabelle requires none such administrative chores of
1.63 +its end-users --- the executables can be run straight away. Usually,
1.64 +users would want to put the Isabelle \texttt{bin} directory into their
1.65 +shell's search path, of course.
1.66 +
1.67 +
1.68 +\subsection{Building the environment}
1.69 +
1.70 +The environment that all Isabelle programs are run in is built as
1.71 +follows:
1.72 +
1.73 +\begin{enumerate}
1.74 +\item The special variable \ttindex{ISABELLE_HOME} is determined
1.75 + automatically from the location of the binary that has been run
1.76 + (e.g.\ \texttt{isabelle}).
1.77 +
1.78 + You should not try to set \texttt{ISABELLE_HOME} manually. Also note
1.79 + that the Isabelle executables have to be run from their original
1.80 + location in the distribution directory --- copying or linking them
1.81 + somewhere else just won't work!
1.82 +
1.83 +\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a GNU
1.84 + bash script with the variable auto-export option enabled.
1.85 +
1.86 + The file typically contains a rather long list of assigments
1.87 + \texttt{FOO="bar"}, thus providing the site default settings. The
1.88 + Isabelle distribution already contains a global settings file with
1.89 + sensible defaults. When installing the system, only a few of these
1.90 + have to be adapted (most likely \texttt{ML_SYSTEM} and friends).
1.91 +
1.92 +\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it
1.93 + exists) is run the same way as the site default settings. The
1.94 + variable \texttt{ISABELLE_HOME_USER} has already been set before ---
1.95 + usually to \texttt{\~\relax/isabelle}.
1.96 +
1.97 + Thus individual users may override the site-wide defaults. See also
1.98 + file \texttt{etc/user-settings.sample} in the distribution.
1.99 + Typically, user settings are a few lines only, just containing the
1.100 + assigments that are really required. One should definitely
1.101 + \emph{not} start with a full copy the central
1.102 + \texttt{\$ISABELLE_HOME/etc/settings}. This may cause severe
1.103 + maintainance problems later, when the Isabelle installation is
1.104 + updated or changed otherwise.
1.105 +
1.106 +\end{enumerate}
1.107 +
1.108 +Note that settings files are actually bash scripts. So one may use
1.109 +complex shell commands, e.g.\ \texttt{if} or \texttt{case} statements
1.110 +to set variables depending on the system architecture or other
1.111 +environment variables. Such advanced features should be added only
1.112 +with great care, though. In particular, external environment
1.113 +references should be kept at a minimum.
1.114 +
1.115 +\medskip A few variables are somewhat:
1.116 +\begin{itemize}
1.117 +\item \ttindex{ISABELLE} and \ttindex{ISATOOL} are set automatically
1.118 + to the absolute path names of the \texttt{isabelle} and
1.119 + \texttt{isatool} executables, respectively.
1.120 +
1.121 +\item \ttindex{ISABELLE_PATH} and \ttindex{ISABELLE_OUTPUT} will have
1.122 + the {\ML} system identifier (as specified by \texttt{ML_SYSTEM})
1.123 + automatically appended to their values.
1.124 +\end{itemize}
1.125 +
1.126 +\medskip The Isabelle settings scheme is basically quite simple, but
1.127 +non-trivial. For debugging purposes, the generated environment may be
1.128 +inspected with the \texttt{getenv} Isabelle tool, see
1.129 +\S\ref{sec:tool-getenv}.
1.130 +
1.131 +
1.132 +\subsection{Common variables}
1.133 +
1.134 +Below is a reference of common Isabelle settings variables. The list
1.135 +is somewhat open-ended, in particular, third-party utilities or
1.136 +interfaces may add their own selection.
1.137 +
1.138 +\begin{ttdescription}
1.139 +\item[FIXME] FIXME
1.140 +\end{ttdescription}
1.141 +
1.142 +
1.143 +\section{Isabelle proper --- \texttt{isabelle}}
1.144 +
1.145 +The \ttindex{isabelle} executable runs logic sessions --- either
1.146 +interactively or in batch mode. It provides an abstraction over the
1.147 +underlying {\ML} system, and over the actual heap file locations. The usage is:
1.148 +\begin{ttbox}
1.149 +Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
1.150 +
1.151 + Options are:
1.152 + -e MLTEXT pass MLTEXT to the ML session
1.153 + -m MODE add print mode for output
1.154 + -q non-interactive session
1.155 + -r open heap file read-only
1.156 +
1.157 + INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
1.158 + These are either names to be searched in the Isabelle path, or actual
1.159 + file names (then containing at least one /).
1.160 + If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
1.161 +\end{ttbox}
1.162 +Input files without path specifications are looked up in the
1.163 +\texttt{ISABELLE_PATH} setting, which may consist of multiple
1.164 +components separated by colons --- these are tried in the given order.
1.165 +Short output names are relative to the directory specified by
1.166 +\texttt{ISABELLE_OUTPUT} setting. In any case, actual file locations
1.167 +can be given by including at least one \texttt{/} (use \texttt{./} to
1.168 +refer to the current directory).
1.169 +
1.170 +If the input heap file is not writable, or the \texttt{-r} option is
1.171 +given explicitely, the session will be read-only. That is, the {\ML}
1.172 +world cannot be committed back into the logic image. A writable
1.173 +session enables commits into either the input file, or into an
1.174 +alternative output heap file which may be given as the second
1.175 +argument.
1.176 +
1.177 +The read-write state of sessions is determined at startup only, it
1.178 +cannot be changed intermediately. Also note that heap images may
1.179 +require considerable amounts of disk space. Users are responsible
1.180 +themselves to dispose no longer needed heap files.
1.181 +
1.182 +
1.183 +\subsection*{Options}
1.184 +
1.185 +Using \texttt{-e} one may pass {\ML} code to the Isabelle session from
1.186 +the command line. Multiple \texttt{-e}'s are evaluated in the given
1.187 +order.
1.188 +
1.189 +The \texttt{-m} option addes print mode identifiers to be made active
1.190 +for this session. Typically this is used by some user interface to
1.191 +enable output of mathematical symbols from a special screen font, for
1.192 +example (see also \S\ref{sec:fonts} about fonts and the \emph{Isabelle
1.193 + Reference Manual} about print modes in general).
1.194 +
1.195 +Isabelle normally enters an interactice {\ML} top-level loop (after
1.196 +processing the \texttt{-e} texts). The \texttt{-q} option inhibits
1.197 +this, providing a pure batch mode facility.
1.198 +
1.199 +
1.200 +\subsection*{Examples}
1.201 +
1.202 +Run an interactive session of the default object-logic:
1.203 +\begin{ttbox}
1.204 +isabelle
1.205 +\end{ttbox}
1.206 +Usually, this refers to one of the standard logic images, which are
1.207 +read-only by default.
1.208 +
1.209 +Run a writable session, based on \texttt{FOL}, but output to
1.210 +\texttt{Foo} (in the directory specified by the
1.211 +\texttt{ISABELLE_OUTPUT} setting):
1.212 +\begin{ttbox}
1.213 +isabelle FOL Foo
1.214 +\end{ttbox}
1.215 +Ending this session normally (e.g.\ by typing control-D), dumps the
1.216 +whole {\ML} system state into \texttt{Foo}. Be prepared for several
1.217 +megabytes!
1.218 +
1.219 +The \texttt{Foo} session may be continued (writably!) at exactly the
1.220 +same point as follows:
1.221 +\begin{ttbox}
1.222 +isabelle Foo
1.223 +\end{ttbox}
1.224 +
1.225 +\medskip This is a simple batch mode example, printing a certain
1.226 +theorem of \texttt{FOL}:
1.227 +\begin{ttbox}
1.228 +isabelle -e "prth allE;" -q -r FOL
1.229 +\end{ttbox}
1.230 +Note that the output text will be usually interspered with some
1.231 +garbage produced by the {\ML} compiler.
1.232 +
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/System/fonts.tex Wed May 14 19:27:21 1997 +0200
2.3 @@ -0,0 +1,21 @@
2.4 +
2.5 +\chapter{Fonts and character encodings}
2.6 +
2.7 +\section{ --- \texttt{isatool installfonts}}
2.8 +
2.9 +\begin{ttbox}
2.10 +Usage: isatool installfonts
2.11 +
2.12 + Install the isabelle fonts into your X11 server.
2.13 + (May be savely called repeatedly.)
2.14 +\end{ttbox}
2.15 +
2.16 +
2.17 +\section{ --- \texttt{isatool symbolinput}}
2.18 +
2.19 +
2.20 +%FIXME not yet
2.21 +%\section{ --- \texttt{isatool showsymbols}}
2.22 +%
2.23 +%\begin{ttbox}
2.24 +%\end{ttbox}
3.1 --- a/doc-src/System/html.tex Wed May 14 18:42:09 1997 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,211 +0,0 @@
3.4 -\chapter{Generating HTML documents} \label{html}
3.5 -\index{HTML|bold}
3.6 -
3.7 -Isabelle is able to make HTML documents that show a theory's
3.8 -definition, the theorems proved in its ML file and the relationship
3.9 -with its ancestors and descendants. HTML stands for Hypertext Markup
3.10 -Language and is used in the World Wide Web to represent text
3.11 -containing images and links to other documents. Web browsers like
3.12 -{\tt xmosaic} or {\tt netscape} are used to view these documents.
3.13 -
3.14 -Besides the three HTML files that are made for every theory
3.15 -(definition and theorems, ancestors, descendants), Isabelle stores
3.16 -links to all theories in an index file. These indexes are themself
3.17 -linked with other indexes to represent the hierarchic structure of
3.18 -Isabelle's logics.
3.19 -
3.20 -To make HTML files for logics that are part of the Isabelle
3.21 -distribution, simply set the shell environment variable {\tt
3.22 -MAKE_HTML} before compiling a logic. This works for single logics as
3.23 -well as for the shell script {\tt make-all} (see
3.24 -\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
3.25 -{\tt csh} style shell, the following commands can be used:
3.26 -
3.27 -\begin{ttbox}
3.28 -cd FOL
3.29 -setenv MAKE_HTML
3.30 -make
3.31 -\end{ttbox}
3.32 -
3.33 -The databases made this way do not differ from the ones made with an
3.34 -unset {\tt MAKE_HTML}; in particular no HTML files are written if the
3.35 -database is used to manually load a theory.
3.36 -
3.37 -As you will see below, the HTML generation is controlled by a boolean
3.38 -reference variable. If you want to make databases which define this
3.39 -variable's value as {\tt true} and where therefore HTML files are
3.40 -written each time {\tt use_thy} is invoked, you have to set {\tt
3.41 -MAKE_HTML} to ``{\tt true}'':
3.42 -
3.43 -\begin{ttbox}
3.44 -cd FOL
3.45 -setenv MAKE_HTML true
3.46 -make
3.47 -\end{ttbox}
3.48 -
3.49 -All theories loaded from within the {\tt FOL} database and all
3.50 -databases derived from it will now cause HTML files to be written.
3.51 -This behaviour can be changed by assigning a value of {\tt false} to
3.52 -the boolean reference variable {\tt make_html}. Be careful when making
3.53 -such databases publicly available since it means that your users will
3.54 -generate HTML files though they might not intend to do so.
3.55 -
3.56 -As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
3.57 -{\tt FOL}) and because the HTML files list a theory's ancestors, you
3.58 -should not make HTML files for a logic if the HTML files for the base
3.59 -logic do not exist. Otherwise some of the hypertext links might point
3.60 -to non-existing documents.
3.61 -
3.62 -The entry point to all logics is the {\tt index.html} file located in
3.63 -Isabelle's main directory. You can also access a HTML version of the
3.64 -distribution package at
3.65 -
3.66 -\begin{ttbox}
3.67 -http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
3.68 -\end{ttbox}
3.69 -
3.70 -
3.71 -\section*{Manual HTML generation}
3.72 -
3.73 -To manually control the generation of HTML files the following
3.74 -commands and reference variables are used:
3.75 -
3.76 -\begin{ttbox}
3.77 -init_html : unit -> unit
3.78 -make_html : bool ref
3.79 -finish_html : unit -> unit
3.80 -\end{ttbox}
3.81 -
3.82 -\begin{ttdescription}
3.83 -\item[\ttindexbold{init_html}]
3.84 -activates the HTML facility. It stores the current working directory
3.85 -as the place where the {\tt index.html} file for all theories loaded
3.86 -afterwards will be stored.
3.87 -
3.88 -\item[\ttindexbold{make_html}]
3.89 -is a boolean reference variable read by {\tt use_thy} and other
3.90 -functions to decide whether HTML files should be made. After you have
3.91 -used {\tt init_html} you can manually change {\tt make_html}'s value
3.92 -to temporarily disable HTML generation.
3.93 -
3.94 -\item[\ttindexbold{finish_html}]
3.95 -has to be called after all theories have been read that should be
3.96 -listed in the current {\tt index.html} file. It reads a temporary
3.97 -file with information about the theories read since the last use of
3.98 -{\tt init_html} and makes the {\tt index.html} file. If {\tt
3.99 -make_html} is {\tt false} nothing is done.
3.100 -
3.101 -The indexes made by this function also contain a link to the {\tt
3.102 -README} file if there exists one in the directory where the index is
3.103 -stored. If there's a {\tt README.html} file it is used instead of
3.104 -{\tt README}.
3.105 -
3.106 -\end{ttdescription}
3.107 -
3.108 -The above functions could be used in the following way:
3.109 -
3.110 -\begin{ttbox}
3.111 -init_html();
3.112 -{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
3.113 -use_thy "List";
3.114 -\dots
3.115 -finish_html();
3.116 -\end{ttbox}
3.117 -
3.118 -Please note that HTML files are made only for those theories that are
3.119 -read while {\tt make_html} is {\tt true}. These files may contain
3.120 -links to theories that were read with a {\tt false} {\tt make_html}
3.121 -and therefore point to non-existing files.
3.122 -
3.123 -
3.124 -\section*{Extending or adding a logic}
3.125 -
3.126 -If you add a new subdirectory to Isabelle's logics (or add a completly
3.127 -new logic), you would have to call {\tt init_html} at the start of every
3.128 -directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
3.129 -it. This is automatically done if you use
3.130 -
3.131 -\begin{ttbox}\index{*use_dir}
3.132 -use_dir : string -> unit
3.133 -\end{ttbox}
3.134 -
3.135 -This function takes a path as its parameter, changes the working
3.136 -directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
3.137 -executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
3.138 -index.html} file written in this directory will be automatically
3.139 -linked to the first index found in the (recursively searched)
3.140 -superdirectories.
3.141 -
3.142 -Instead of adding something like
3.143 -
3.144 -\begin{ttbox}
3.145 -use"ex/ROOT.ML";
3.146 -\end{ttbox}
3.147 -
3.148 -to the logic's makefile you have to use this:
3.149 -
3.150 -\begin{ttbox}
3.151 -use_dir"ex";
3.152 -\end{ttbox}
3.153 -
3.154 -Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
3.155 -{\tt true} the generation of HTML files depends on the value this
3.156 -reference variable has. It can either be inherited from the used \ML{}
3.157 -database or set in the makefile before {\tt use_dir} is invoked,
3.158 -e.g. to set it's value according to the environment variable {\tt
3.159 -MAKE_HTML}.
3.160 -
3.161 -The generated HTML files contain all theorems that were proved in the
3.162 -theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
3.163 -or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
3.164 -is a hypertext link to the whole \ML{} file.
3.165 -
3.166 -You can add section headings to the list of theorems by using
3.167 -
3.168 -\begin{ttbox}\index{*use_dir}
3.169 -section: string -> unit
3.170 -\end{ttbox}
3.171 -
3.172 -in a theory's ML file, which converts a plain string to a HTML
3.173 -heading and inserts it before the next theorem proved or stored with
3.174 -one of the above functions. If {\tt make_html} is {\tt false} nothing
3.175 -is done.
3.176 -
3.177 -
3.178 -\section*{Using someone else's database}
3.179 -
3.180 -To make them independent from their storage place, the HTML files only
3.181 -contain relative paths which are derived from absolute ones like the
3.182 -current working directory, {\tt gif_path} or {\tt base_path}. The
3.183 -latter two are reference variables which are initialized at the time
3.184 -when the {\tt Pure} database is made. Because you need write access
3.185 -for the current directory to make HTML files and therefore (probably)
3.186 -generate them in your home directory, the absolute {\tt base_path} is
3.187 -not correct if you use someone else's database or a database derived
3.188 -from it.
3.189 -
3.190 -In that case you first should set {\tt base_path} to the value of {\em
3.191 -your} Isabelle main directory, i.e. the directory that contains the
3.192 -subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
3.193 -your own logics are stored. If you do not do this, the generated HTML
3.194 -files will still be usable but may contain incomplete titles and lack
3.195 -some hypertext links.
3.196 -
3.197 -It's also a good idea to set {\tt gif_path} which points to the
3.198 -directory containing two GIF images used in the HTML
3.199 -documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
3.200 -main directory. While its value in general is still valid, your HTML
3.201 -files would depend on files not owned by you. This prevents you from
3.202 -changing the location of the HTML files (as they contain relative
3.203 -paths) and also causes trouble if the database's maker (re)moves the
3.204 -GIFs.
3.205 -
3.206 -Here's what you should do before invoking {\tt init_html} using
3.207 -someone else's \ML{} database:
3.208 -
3.209 -\begin{ttbox}
3.210 -base_path := "/home/smith/isabelle";
3.211 -gif_path := "/home/smith/isabelle/Tools";
3.212 -init_html();
3.213 -\dots
3.214 -\end{ttbox}
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/System/misc.tex Wed May 14 19:27:21 1997 +0200
4.3 @@ -0,0 +1,111 @@
4.4 +
4.5 +% $Id$
4.6 +
4.7 +\chapter{Miscellaneous tools}
4.8 +
4.9 +
4.10 +\section{Inspecting the settings environment -- \texttt{isatool getenv}}
4.11 +\label{sec:tool-getenv}
4.12 +
4.13 +The Isabelle settings environment --- as provided by the site-default
4.14 +and user-specific settings files --- can be inspected with the
4.15 +\tooldx{getenv} utility:
4.16 +\begin{ttbox}
4.17 +Usage: isatool getenv [OPTIONS] [VARNAMES ...]
4.18 +
4.19 + Options are:
4.20 + -a display complete environment
4.21 + -b print values only (doesn't work for -a)
4.22 +
4.23 + Get value of VARNAMES from the Isabelle settings.
4.24 +\end{ttbox}
4.25 +
4.26 +With the \texttt{-a} option, one may inspect the full process
4.27 +environment that Isabelle related programs are run in. This usually
4.28 +contains much more variables than are actually Isabelle settings.
4.29 +
4.30 +Unless the \texttt{-b} option is given, the output is a list of lines
4.31 +of the form $varname\mathtt{=}value$.
4.32 +
4.33 +
4.34 +\subsection*{Examples}
4.35 +
4.36 +Get the {\ML} system identifier and the location where the compiler
4.37 +binaries are supposed to be installed as follows:
4.38 +\begin{ttbox}
4.39 +isatool getenv ML_SYSTEM ML_HOME
4.40 +{\out ML_HOME=/usr/local/sml109.27/bin}
4.41 +{\out ML_SYSTEM=smlnj-1.09}
4.42 +\end{ttbox}
4.43 +
4.44 +This one peeks at the search path that \texttt{isabelle} uses to
4.45 +locate logic images:
4.46 +\begin{ttbox}
4.47 +isatool getenv -b ISABELLE_PATH
4.48 +{\out /home/mmw/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09}
4.49 +\end{ttbox}
4.50 +We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=}
4.51 +prefix. The value above is what became of the following assignment in
4.52 +the default settings file:
4.53 +\begin{ttbox}
4.54 +ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps
4.55 +\end{ttbox}
4.56 +Note how \texttt{\$ML_SYSTEM} got appended automatically to each path
4.57 +component. This is a special feature of \texttt{ISABELLE_PATH} (and
4.58 +also of \texttt{ISABELLE_OUTPUT}).
4.59 +
4.60 +\section{Get logic images --- \texttt{isatool findlogics}}
4.61 +
4.62 +\begin{ttbox}
4.63 +Usage: isatool findlogics
4.64 +
4.65 + Collect heap file names from ISABELLE_PATH.
4.66 +\end{ttbox}
4.67 +
4.68 +\section{Isabelle's version of make --- \texttt{isatool make}}
4.69 +
4.70 +\begin{ttbox}
4.71 +Usage: isatool make [ARGS ...]
4.72 +
4.73 + Compiles logic in current directory using IsaMakefile.
4.74 + ARGS are directly passed to the system make program.
4.75 +\end{ttbox}
4.76 +
4.77 +
4.78 +\section{ --- \texttt{isatool usedir}}
4.79 +
4.80 +\begin{ttbox}
4.81 +Usage: isatool usedir LOGIC NAME
4.82 +
4.83 + Options are:
4.84 + -b build mode (output heap image, use dir ".")
4.85 + -g BOOL generate theory graph data (default false)
4.86 + -h BOOL generate theory HTML data (default false)
4.87 + -s NAME override session NAME
4.88 +
4.89 + Build object-logic or run examples. Also creates browsing
4.90 + information (HTML etc.) according to settings.
4.91 +\end{ttbox}
4.92 +
4.93 +
4.94 +\section{ --- \texttt{isatool doc}}
4.95 +
4.96 +\begin{ttbox}
4.97 +Usage: isatool doc [DOC]
4.98 +
4.99 + View Isabelle documentation DOC, or show list of available documents.
4.100 +\end{ttbox}
4.101 +
4.102 +
4.103 +\section{ --- \texttt{isatool expandshort}}
4.104 +
4.105 +\begin{ttbox}
4.106 +Usage: expandshort [FILES ...]
4.107 +
4.108 + Expand shorthand goal commands in FILES. Also contracts uses of
4.109 + resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on
4.110 + 1-element lists; furthermore expands tabs, since they are now
4.111 + forbidden in ML string constants.
4.112 +
4.113 + Renames old versions of FILES by appending "~~".
4.114 +\end{ttbox}
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/System/present.tex Wed May 14 19:27:21 1997 +0200
5.3 @@ -0,0 +1,214 @@
5.4 +
5.5 +\chapter{Presenting theories}
5.6 +
5.7 +\section{Generating HTML documents} \label{sec:html}
5.8 +\index{HTML|bold}
5.9 +
5.10 +Isabelle is able to make HTML documents that show a theory's
5.11 +definition, the theorems proved in its ML file and the relationship
5.12 +with its ancestors and descendants. HTML stands for Hypertext Markup
5.13 +Language and is used in the World Wide Web to represent text
5.14 +containing images and links to other documents. Web browsers like
5.15 +{\tt xmosaic} or {\tt netscape} are used to view these documents.
5.16 +
5.17 +Besides the three HTML files that are made for every theory
5.18 +(definition and theorems, ancestors, descendants), Isabelle stores
5.19 +links to all theories in an index file. These indexes are themself
5.20 +linked with other indexes to represent the hierarchic structure of
5.21 +Isabelle's logics.
5.22 +
5.23 +To make HTML files for logics that are part of the Isabelle
5.24 +distribution, simply set the shell environment variable {\tt
5.25 +MAKE_HTML} before compiling a logic. This works for single logics as
5.26 +well as for the shell script {\tt make-all} (see
5.27 +\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
5.28 +{\tt csh} style shell, the following commands can be used:
5.29 +
5.30 +\begin{ttbox}
5.31 +cd FOL
5.32 +setenv MAKE_HTML
5.33 +make
5.34 +\end{ttbox}
5.35 +
5.36 +The databases made this way do not differ from the ones made with an
5.37 +unset {\tt MAKE_HTML}; in particular no HTML files are written if the
5.38 +database is used to manually load a theory.
5.39 +
5.40 +As you will see below, the HTML generation is controlled by a boolean
5.41 +reference variable. If you want to make databases which define this
5.42 +variable's value as {\tt true} and where therefore HTML files are
5.43 +written each time {\tt use_thy} is invoked, you have to set {\tt
5.44 +MAKE_HTML} to ``{\tt true}'':
5.45 +
5.46 +\begin{ttbox}
5.47 +cd FOL
5.48 +setenv MAKE_HTML true
5.49 +make
5.50 +\end{ttbox}
5.51 +
5.52 +All theories loaded from within the {\tt FOL} database and all
5.53 +databases derived from it will now cause HTML files to be written.
5.54 +This behaviour can be changed by assigning a value of {\tt false} to
5.55 +the boolean reference variable {\tt make_html}. Be careful when making
5.56 +such databases publicly available since it means that your users will
5.57 +generate HTML files though they might not intend to do so.
5.58 +
5.59 +As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
5.60 +{\tt FOL}) and because the HTML files list a theory's ancestors, you
5.61 +should not make HTML files for a logic if the HTML files for the base
5.62 +logic do not exist. Otherwise some of the hypertext links might point
5.63 +to non-existing documents.
5.64 +
5.65 +The entry point to all logics is the {\tt index.html} file located in
5.66 +Isabelle's main directory. You can also access a HTML version of the
5.67 +distribution package at
5.68 +
5.69 +\begin{ttbox}
5.70 +http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
5.71 +\end{ttbox}
5.72 +
5.73 +
5.74 +\section*{Manual HTML generation}
5.75 +
5.76 +To manually control the generation of HTML files the following
5.77 +commands and reference variables are used:
5.78 +
5.79 +\begin{ttbox}
5.80 +init_html : unit -> unit
5.81 +make_html : bool ref
5.82 +finish_html : unit -> unit
5.83 +\end{ttbox}
5.84 +
5.85 +\begin{ttdescription}
5.86 +\item[\ttindexbold{init_html}]
5.87 +activates the HTML facility. It stores the current working directory
5.88 +as the place where the {\tt index.html} file for all theories loaded
5.89 +afterwards will be stored.
5.90 +
5.91 +\item[\ttindexbold{make_html}]
5.92 +is a boolean reference variable read by {\tt use_thy} and other
5.93 +functions to decide whether HTML files should be made. After you have
5.94 +used {\tt init_html} you can manually change {\tt make_html}'s value
5.95 +to temporarily disable HTML generation.
5.96 +
5.97 +\item[\ttindexbold{finish_html}]
5.98 +has to be called after all theories have been read that should be
5.99 +listed in the current {\tt index.html} file. It reads a temporary
5.100 +file with information about the theories read since the last use of
5.101 +{\tt init_html} and makes the {\tt index.html} file. If {\tt
5.102 +make_html} is {\tt false} nothing is done.
5.103 +
5.104 +The indexes made by this function also contain a link to the {\tt
5.105 +README} file if there exists one in the directory where the index is
5.106 +stored. If there's a {\tt README.html} file it is used instead of
5.107 +{\tt README}.
5.108 +
5.109 +\end{ttdescription}
5.110 +
5.111 +The above functions could be used in the following way:
5.112 +
5.113 +\begin{ttbox}
5.114 +init_html();
5.115 +{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
5.116 +use_thy "List";
5.117 +\dots
5.118 +finish_html();
5.119 +\end{ttbox}
5.120 +
5.121 +Please note that HTML files are made only for those theories that are
5.122 +read while {\tt make_html} is {\tt true}. These files may contain
5.123 +links to theories that were read with a {\tt false} {\tt make_html}
5.124 +and therefore point to non-existing files.
5.125 +
5.126 +
5.127 +\section*{Extending or adding a logic}
5.128 +
5.129 +If you add a new subdirectory to Isabelle's logics (or add a completly
5.130 +new logic), you would have to call {\tt init_html} at the start of every
5.131 +directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
5.132 +it. This is automatically done if you use
5.133 +
5.134 +\begin{ttbox}\index{*use_dir}
5.135 +use_dir : string -> unit
5.136 +\end{ttbox}
5.137 +
5.138 +This function takes a path as its parameter, changes the working
5.139 +directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
5.140 +executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
5.141 +index.html} file written in this directory will be automatically
5.142 +linked to the first index found in the (recursively searched)
5.143 +superdirectories.
5.144 +
5.145 +Instead of adding something like
5.146 +
5.147 +\begin{ttbox}
5.148 +use"ex/ROOT.ML";
5.149 +\end{ttbox}
5.150 +
5.151 +to the logic's makefile you have to use this:
5.152 +
5.153 +\begin{ttbox}
5.154 +use_dir"ex";
5.155 +\end{ttbox}
5.156 +
5.157 +Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
5.158 +{\tt true} the generation of HTML files depends on the value this
5.159 +reference variable has. It can either be inherited from the used \ML{}
5.160 +database or set in the makefile before {\tt use_dir} is invoked,
5.161 +e.g. to set it's value according to the environment variable {\tt
5.162 +MAKE_HTML}.
5.163 +
5.164 +The generated HTML files contain all theorems that were proved in the
5.165 +theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
5.166 +or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
5.167 +is a hypertext link to the whole \ML{} file.
5.168 +
5.169 +You can add section headings to the list of theorems by using
5.170 +
5.171 +\begin{ttbox}\index{*use_dir}
5.172 +section: string -> unit
5.173 +\end{ttbox}
5.174 +
5.175 +in a theory's ML file, which converts a plain string to a HTML
5.176 +heading and inserts it before the next theorem proved or stored with
5.177 +one of the above functions. If {\tt make_html} is {\tt false} nothing
5.178 +is done.
5.179 +
5.180 +
5.181 +\section*{Using someone else's database}
5.182 +
5.183 +To make them independent from their storage place, the HTML files only
5.184 +contain relative paths which are derived from absolute ones like the
5.185 +current working directory, {\tt gif_path} or {\tt base_path}. The
5.186 +latter two are reference variables which are initialized at the time
5.187 +when the {\tt Pure} database is made. Because you need write access
5.188 +for the current directory to make HTML files and therefore (probably)
5.189 +generate them in your home directory, the absolute {\tt base_path} is
5.190 +not correct if you use someone else's database or a database derived
5.191 +from it.
5.192 +
5.193 +In that case you first should set {\tt base_path} to the value of {\em
5.194 +your} Isabelle main directory, i.e. the directory that contains the
5.195 +subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
5.196 +your own logics are stored. If you do not do this, the generated HTML
5.197 +files will still be usable but may contain incomplete titles and lack
5.198 +some hypertext links.
5.199 +
5.200 +It's also a good idea to set {\tt gif_path} which points to the
5.201 +directory containing two GIF images used in the HTML
5.202 +documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
5.203 +main directory. While its value in general is still valid, your HTML
5.204 +files would depend on files not owned by you. This prevents you from
5.205 +changing the location of the HTML files (as they contain relative
5.206 +paths) and also causes trouble if the database's maker (re)moves the
5.207 +GIFs.
5.208 +
5.209 +Here's what you should do before invoking {\tt init_html} using
5.210 +someone else's \ML{} database:
5.211 +
5.212 +\begin{ttbox}
5.213 +base_path := "/home/smith/isabelle";
5.214 +gif_path := "/home/smith/isabelle/Tools";
5.215 +init_html();
5.216 +\dots
5.217 +\end{ttbox}
6.1 --- a/doc-src/System/system.ind Wed May 14 18:42:09 1997 +0200
6.2 +++ b/doc-src/System/system.ind Wed May 14 19:27:21 1997 +0200
6.3 @@ -1,25 +1,42 @@
6.4 \begin{theindex}
6.5
6.6 - \item browser, \bold{5}
6.7 + \item browser, \bold{14}
6.8
6.9 \indexspace
6.10
6.11 - \item {\tt finish_html}, \bold{2}
6.12 + \item {\tt finish_html}, \bold{11}
6.13 +
6.14 + \indexspace
6.15 +
6.16 + \item {\tt getenv} tool, 5
6.17 +
6.18 + \indexspace
6.19 +
6.20 + \item HTML, \bold{10}
6.21
6.22 \indexspace
6.23
6.24 - \item HTML, \bold{1}
6.25 -
6.26 - \indexspace
6.27 -
6.28 - \item {\tt init_html}, \bold{2}
6.29 + \item {\tt init_html}, \bold{11}
6.30 + \item {\tt INSTALL}, 1
6.31 + \item {\tt ISABELLE}, 3
6.32 + \item {\tt Isabelle}, 1
6.33 + \item {\tt isabelle}, 1, 3
6.34 + \item {\tt ISABELLE_HOME}, 2
6.35 + \item {\tt ISABELLE_OUTPUT}, 3
6.36 + \item {\tt ISABELLE_PATH}, 3
6.37 + \item {\tt ISATOOL}, 3
6.38 + \item {\tt isatool}, 1
6.39
6.40 \indexspace
6.41
6.42 - \item {\tt make_html}, \bold{2}
6.43 + \item {\tt make_html}, \bold{11}
6.44
6.45 \indexspace
6.46
6.47 - \item {\tt use_dir}, 3
6.48 + \item settings, \bold{1}
6.49 +
6.50 + \indexspace
6.51 +
6.52 + \item {\tt use_dir}, 12
6.53
6.54 \end{theindex}
7.1 --- a/doc-src/System/system.tex Wed May 14 18:42:09 1997 +0200
7.2 +++ b/doc-src/System/system.tex Wed May 14 19:27:21 1997 +0200
7.3 @@ -17,7 +17,7 @@
7.4 With Contributions by Tobias Nipkow and Markus Wenzel%
7.5 \thanks{Chapter~\protect\ref{html} was written by Carsten
7.6 Clasohm. Chapter~\protect\ref{browse} was written by Stefan
7.7 - Berghofer. Some other parts are by Markus Wenzel.}}
7.8 + Berghofer. Other parts are by Markus Wenzel.}}
7.9
7.10 \makeindex
7.11
7.12 @@ -35,7 +35,10 @@
7.13
7.14 %\include{introduction}
7.15
7.16 -\include{html}
7.17 +\include{basics}
7.18 +\include{misc}
7.19 +\include{fonts}
7.20 +\include{present}
7.21 \include{browse}
7.22
7.23 %\begingroup