doc-src/System/present.tex

still under construction!

\chapter{Presenting theories}

\section{Generating HTML documents} \label{sec:html}
\index{HTML|bold} 

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 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
links to all theories in an index file. These indexes are themself
linked with other indexes to represent the hierarchic structure of
Isabelle's logics.

\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}
ISABELLE_USEDIR_OPTIONS="-h true"
\end{ttbox}
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}).

\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.

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*{*HTML generation internals}

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
finish_html : unit -> unit
\end{ttbox}

\begin{ttdescription}
\item[\ttindexbold{init_html}]
activates the HTML facility. It stores the current working directory
as the place where the {\tt index.html} file for all theories loaded
afterwards will be stored.

\item[\ttindexbold{make_html}]
is a boolean reference variable read by {\tt use_thy} and other
functions to decide whether HTML files should be made. After you have
used {\tt init_html} you can manually change {\tt make_html}'s value
to temporarily disable HTML generation.

\item[\ttindexbold{finish_html}]
has to be called after all theories have been read that should be
listed in the current {\tt index.html} file. It reads a temporary
file with information about the theories read since the last use of
{\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
\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}

The above functions could be used in the following way:

\begin{ttbox}
init_html();
{\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 \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
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
\end{ttbox}

This function takes a path as its parameter, changes the working
directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
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)
super directories.

The \texttt{usedir} utility (see also \S\ref{sec:tool-usedir}) will
automatically take care of this.

\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

\begin{ttbox}\index{*use_dir}
section: string -> unit
\end{ttbox}

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.


\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
current working directory, {\tt gif_path} or {\tt base_path}. The
latter two are reference variables which are initialized at the time
when the {\tt Pure} database is made. Because you need write access
for the current directory to make HTML files and therefore (probably)
generate them in your home directory, the absolute {\tt base_path} is
not correct if you use someone else's database or a database derived
from it.

In that case you first should set {\tt base_path} to the value of {\em
your} Isabelle main directory, i.e. the directory that contains the
subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
your own logics are stored. If you do not do this, the generated HTML
files will still be usable but may contain incomplete titles and lack
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 \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
paths) and also causes trouble if the database's maker (re)moves the
GIFs.

Here's what you should do before invoking {\tt init_html} using
someone else's \ML{} database:

\begin{ttbox}
base_path := "/home/someone/Isabelle-dist/src";
gif_path := "/home/someone/Isabelle-dist/src/Tools";
init_html();
\dots
\end{ttbox}