doc-src/System/present.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/present.tex	Wed May 14 19:27:21 1997 +0200
@@ -0,0 +1,214 @@
+
+\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 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.
+
+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.
+
+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:
+
+\begin{ttbox}
+cd FOL
+setenv MAKE_HTML
+make
+\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.
+
+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.
+
+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
+
+\begin{ttbox}
+http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
+\end{ttbox}
+
+
+\section*{Manual HTML generation}
+
+To manually control the generation of HTML files the following
+commands and reference variables are used:
+
+\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 {\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}.
+
+\end{ttdescription}
+
+The above functions could be used in the following way:
+
+\begin{ttbox}
+init_html();
+{\out Setting path for index.html to "/home/clasohm/isabelle/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.
+
+
+\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
+
+\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)
+superdirectories.
+
+Instead of adding something like
+
+\begin{ttbox}
+use"ex/ROOT.ML";
+\end{ttbox}
+
+to the logic's makefile you have to use 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.
+
+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. If {\tt make_html} is {\tt false} nothing
+is done.
+
+
+\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 {\tt 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/smith/isabelle";
+gif_path := "/home/smith/isabelle/Tools";
+init_html();
+\dots
+\end{ttbox}