preliminary!
authorwenzelm
Wed May 14 19:27:21 1997 +0200 (1997-05-14)
changeset 3188445555a7b714
parent 3187 8f8c88dcd728
child 3189 50f42a1d7fb9
preliminary!
doc-src/System/basics.tex
doc-src/System/fonts.tex
doc-src/System/html.tex
doc-src/System/misc.tex
doc-src/System/present.tex
doc-src/System/system.ind
doc-src/System/system.tex
     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