Modified section about generation of theory browsing information.
Documented new -P option.
--- a/doc-src/System/present.tex Wed Aug 18 12:23:10 1999 +0200
+++ b/doc-src/System/present.tex Wed Aug 18 15:40:45 1999 +0200
@@ -8,16 +8,12 @@
Isabelle is able to generate theory browsing information, such as 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 links to other documents. These documents
-may be viewed using Web browsers like Netscape or Lynx.
+ML file and the relationship with its ancestors and descendants.
-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.
+Besides the HTML file that is generated for every theory, 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.
In addition to the HTML files, Isabelle also generates \emph{graph}
files that represent the theory hierarchy of a logic. These graphs
@@ -43,13 +39,6 @@
\medskip The directory in which to store theory browsing information
is determined by the \settdx{ISABELLE_BROWSER_INFO} setting.
-
-\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
the directory denoted by \texttt{ISABELLE_BROWSER_INFO}.
@@ -65,32 +54,18 @@
Of course, this is not necessarily consistent with your local version!
+\medskip
To present your own theories on the WWW, simply copy the whole
\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server.
-
-
-\section{Extending or adding a logic}
-
-If you add a new subdirectory to Isabelle's logics (or add a
-completely new logic), provide a {\tt ROOT.ML} file which reads in the
-theory files. The {\tt ROOT.ML} file will then be processed via the
-function
-
-\begin{ttbox}\index{*use_dir}
-use_dir : string -> unit
+When running your theories with the \texttt{usedir} utility, you can
+generate browsing information by specifying the option \texttt{-i true}
+on the command line, e.g.
+\begin{ttbox}
+isatool usedir -i true HOL my_theories
\end{ttbox}
-which takes a path as its parameter, changes the working directory,
-executes {\tt ROOT.ML}, and makes sure that theory browsing
-information is generated properly. 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
+The generated HTML files contain all theorems that were
+proved in the theories' \ML{} files 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.
@@ -104,45 +79,18 @@
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}
-
+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. If the HTML files for the
+base logic are located in a directory other than \texttt{ISABELLE_BROWSER_INFO}
+or on a WWW server, you have to specify this directory or URL via
+the \texttt{-P} option, e.g.
+\begin{ttbox}
+isatool usedir -i true
+ -P http://isabelle.in.tum.de/library/ HOL my_theories
+\end{ttbox}
\section{Browsing theory graphs} \label{sec:browse}
\index{theory graph browser|bold}