author clasohm Thu, 15 Feb 1996 10:51:22 +0100 changeset 1497 41a1b0426b2e parent 1496 c443b2adaf52 child 1498 7b7d20e89b1b
updated documentation of MAKE_HTML
 doc-src/Ref/theories.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/theories.tex	Thu Feb 15 08:10:36 1996 +0100
+++ b/doc-src/Ref/theories.tex	Thu Feb 15 10:51:22 1996 +0100
@@ -484,22 +484,30 @@
make
\end{ttbox}

-When using ML databases made this way to load additional theories or
-derive other databases from them, you have to be aware that HTML
-generation remains activated. Also be especially careful when making
+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 might
get into trouble that they don't expect, like IO exceptions caused by
insufficient write access.

-The reason is that the boolean reference variable {\tt make_html} (see
-below) is set. Therefore HTML files are generated unless you assign a
-value of {\tt false} to {\tt make_html}.
-
-This is not influenced by the environment variable {\tt MAKE_HTML},
-because the only place where it is used is in the makefile where it
-determines the initial value of {\tt make_html} for a newly made
-database.
-
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
@@ -546,7 +554,7 @@
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 were the index is
+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
finish_html();