1.1 --- a/doc-src/Ref/theories.tex Thu May 15 14:58:51 1997 +0200
1.2 +++ b/doc-src/Ref/theories.tex Thu May 15 14:59:25 1997 +0200
1.3 @@ -1,3 +1,4 @@
1.4 +
1.5 %% $Id$
1.6
1.7 \chapter{Theories, Terms and Types} \label{theories}
1.8 @@ -300,20 +301,6 @@
1.9 \end{ttdescription}
1.10
1.11
1.12 -%FIXME remove
1.13 -%\goodbreak
1.14 -%\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
1.15 -%The theory mechanism depends upon reference variables. At the end of a
1.16 -%Poly/\ML{} session, the contents of references are lost unless they are
1.17 -%declared in the current database. In particular, assignments to references
1.18 -%of the {\tt Pure} database are lost, including all information about loaded
1.19 -%theories. To avoid losing this information simply call
1.20 -%\begin{ttbox}
1.21 -%init_thy_reader();
1.22 -%\end{ttbox}
1.23 -%when building the new database.
1.24 -
1.25 -
1.26 \subsection{*Pseudo theories}\label{sec:pseudo-theories}
1.27 \indexbold{theories!pseudo}%
1.28 Any automatic reloading facility requires complete knowledge of all
1.29 @@ -512,219 +499,6 @@
1.30 with~$thy$.
1.31 \end{ttdescription}
1.32
1.33 -%FIXME move to sysman!
1.34 -%\section{Generating HTML documents}
1.35 -%\index{HTML|bold}
1.36 -%
1.37 -%Isabelle is able to make HTML documents that show a theory's
1.38 -%definition, the theorems proved in its ML file and the relationship
1.39 -%with its ancestors and descendants. HTML stands for Hypertext Markup
1.40 -%Language and is used in the World Wide Web to represent text
1.41 -%containing images and links to other documents. Web browsers like
1.42 -%{\tt xmosaic} or {\tt netscape} are used to view these documents.
1.43 -%
1.44 -%Besides the three HTML files that are made for every theory
1.45 -%(definition and theorems, ancestors, descendants), Isabelle stores
1.46 -%links to all theories in an index file. These indexes are themself
1.47 -%linked with other indexes to represent the hierarchic structure of
1.48 -%Isabelle's logics.
1.49 -%
1.50 -%To make HTML files for logics that are part of the Isabelle
1.51 -%distribution, simply set the shell environment variable {\tt
1.52 -%MAKE_HTML} before compiling a logic. This works for single logics as
1.53 -%well as for the shell script {\tt make-all} (see
1.54 -%\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
1.55 -%{\tt csh} style shell, the following commands can be used:
1.56 -%
1.57 -%\begin{ttbox}
1.58 -%cd FOL
1.59 -%setenv MAKE_HTML
1.60 -%make
1.61 -%\end{ttbox}
1.62 -%
1.63 -%The databases made this way do not differ from the ones made with an
1.64 -%unset {\tt MAKE_HTML}; in particular no HTML files are written if the
1.65 -%database is used to manually load a theory.
1.66 -%
1.67 -%As you will see below, the HTML generation is controlled by a boolean
1.68 -%reference variable. If you want to make databases which define this
1.69 -%variable's value as {\tt true} and where therefore HTML files are
1.70 -%written each time {\tt use_thy} is invoked, you have to set {\tt
1.71 -%MAKE_HTML} to ``{\tt true}'':
1.72 -%
1.73 -%\begin{ttbox}
1.74 -%cd FOL
1.75 -%setenv MAKE_HTML true
1.76 -%make
1.77 -%\end{ttbox}
1.78 -%
1.79 -%All theories loaded from within the {\tt FOL} database and all
1.80 -%databases derived from it will now cause HTML files to be written.
1.81 -%This behaviour can be changed by assigning a value of {\tt false} to
1.82 -%the boolean reference variable {\tt make_html}. Be careful when making
1.83 -%such databases publicly available since it means that your users will
1.84 -%generate HTML files though they might not intend to do so.
1.85 -%
1.86 -%As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
1.87 -%{\tt FOL}) and because the HTML files list a theory's ancestors, you
1.88 -%should not make HTML files for a logic if the HTML files for the base
1.89 -%logic do not exist. Otherwise some of the hypertext links might point
1.90 -%to non-existing documents.
1.91 -%
1.92 -%The entry point to all logics is the {\tt index.html} file located in
1.93 -%Isabelle's main directory. You can also access a HTML version of the
1.94 -%distribution package at
1.95 -%
1.96 -%\begin{ttbox}
1.97 -%http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
1.98 -%\end{ttbox}
1.99 -%
1.100 -%
1.101 -%\subsection*{Manual HTML generation}
1.102 -%
1.103 -%To manually control the generation of HTML files the following
1.104 -%commands and reference variables are used:
1.105 -%
1.106 -%\begin{ttbox}
1.107 -%init_html : unit -> unit
1.108 -%make_html : bool ref
1.109 -%finish_html : unit -> unit
1.110 -%\end{ttbox}
1.111 -%
1.112 -%\begin{ttdescription}
1.113 -%\item[\ttindexbold{init_html}]
1.114 -%activates the HTML facility. It stores the current working directory
1.115 -%as the place where the {\tt index.html} file for all theories loaded
1.116 -%afterwards will be stored.
1.117 -%
1.118 -%\item[\ttindexbold{make_html}]
1.119 -%is a boolean reference variable read by {\tt use_thy} and other
1.120 -%functions to decide whether HTML files should be made. After you have
1.121 -%used {\tt init_html} you can manually change {\tt make_html}'s value
1.122 -%to temporarily disable HTML generation.
1.123 -%
1.124 -%\item[\ttindexbold{finish_html}]
1.125 -%has to be called after all theories have been read that should be
1.126 -%listed in the current {\tt index.html} file. It reads a temporary
1.127 -%file with information about the theories read since the last use of
1.128 -%{\tt init_html} and makes the {\tt index.html} file. If {\tt
1.129 -%make_html} is {\tt false} nothing is done.
1.130 -%
1.131 -%The indexes made by this function also contain a link to the {\tt
1.132 -%README} file if there exists one in the directory where the index is
1.133 -%stored. If there's a {\tt README.html} file it is used instead of
1.134 -%{\tt README}.
1.135 -%
1.136 -%\end{ttdescription}
1.137 -%
1.138 -%The above functions could be used in the following way:
1.139 -%
1.140 -%\begin{ttbox}
1.141 -%init_html();
1.142 -%{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
1.143 -%use_thy "List";
1.144 -%\dots
1.145 -%finish_html();
1.146 -%\end{ttbox}
1.147 -%
1.148 -%Please note that HTML files are made only for those theories that are
1.149 -%read while {\tt make_html} is {\tt true}. These files may contain
1.150 -%links to theories that were read with a {\tt false} {\tt make_html}
1.151 -%and therefore point to non-existing files.
1.152 -%
1.153 -%
1.154 -%\subsection*{Extending or adding a logic}
1.155 -%
1.156 -%If you add a new subdirectory to Isabelle's logics (or add a completly
1.157 -%new logic), you would have to call {\tt init_html} at the start of every
1.158 -%directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
1.159 -%it. This is automatically done if you use
1.160 -%
1.161 -%\begin{ttbox}\index{use_dir}
1.162 -%use_dir : string -> unit
1.163 -%\end{ttbox}
1.164 -%
1.165 -%This function takes a path as its parameter, changes the working
1.166 -%directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
1.167 -%executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
1.168 -%index.html} file written in this directory will be automatically
1.169 -%linked to the first index found in the (recursively searched)
1.170 -%superdirectories.
1.171 -%
1.172 -%Instead of adding something like
1.173 -%
1.174 -%\begin{ttbox}
1.175 -%use"ex/ROOT.ML";
1.176 -%\end{ttbox}
1.177 -%
1.178 -%to the logic's makefile you have to use this:
1.179 -%
1.180 -%\begin{ttbox}
1.181 -%use_dir"ex";
1.182 -%\end{ttbox}
1.183 -%
1.184 -%Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
1.185 -%{\tt true} the generation of HTML files depends on the value this
1.186 -%reference variable has. It can either be inherited from the used \ML{}
1.187 -%database or set in the makefile before {\tt use_dir} is invoked,
1.188 -%e.g. to set it's value according to the environment variable {\tt
1.189 -%MAKE_HTML}.
1.190 -%
1.191 -%The generated HTML files contain all theorems that were proved in the
1.192 -%theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
1.193 -%or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
1.194 -%is a hypertext link to the whole \ML{} file.
1.195 -%
1.196 -%You can add section headings to the list of theorems by using
1.197 -%
1.198 -%\begin{ttbox}\index{use_dir}
1.199 -%section: string -> unit
1.200 -%\end{ttbox}
1.201 -%
1.202 -%in a theory's ML file, which converts a plain string to a HTML
1.203 -%heading and inserts it before the next theorem proved or stored with
1.204 -%one of the above functions. If {\tt make_html} is {\tt false} nothing
1.205 -%is done.
1.206 -%
1.207 -%
1.208 -%\subsection*{Using someone else's database}
1.209 -%
1.210 -%To make them independent from their storage place, the HTML files only
1.211 -%contain relative paths which are derived from absolute ones like the
1.212 -%current working directory, {\tt gif_path} or {\tt base_path}. The
1.213 -%latter two are reference variables which are initialized at the time
1.214 -%when the {\tt Pure} database is made. Because you need write access
1.215 -%for the current directory to make HTML files and therefore (probably)
1.216 -%generate them in your home directory, the absolute {\tt base_path} is
1.217 -%not correct if you use someone else's database or a database derived
1.218 -%from it.
1.219 -%
1.220 -%In that case you first should set {\tt base_path} to the value of {\em
1.221 -%your} Isabelle main directory, i.e. the directory that contains the
1.222 -%subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
1.223 -%your own logics are stored. If you do not do this, the generated HTML
1.224 -%files will still be usable but may contain incomplete titles and lack
1.225 -%some hypertext links.
1.226 -%
1.227 -%It's also a good idea to set {\tt gif_path} which points to the
1.228 -%directory containing two GIF images used in the HTML
1.229 -%documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
1.230 -%main directory. While its value in general is still valid, your HTML
1.231 -%files would depend on files not owned by you. This prevents you from
1.232 -%changing the location of the HTML files (as they contain relative
1.233 -%paths) and also causes trouble if the database's maker (re)moves the
1.234 -%GIFs.
1.235 -%
1.236 -%Here's what you should do before invoking {\tt init_html} using
1.237 -%someone else's \ML{} database:
1.238 -%
1.239 -%\begin{ttbox}
1.240 -%base_path := "/home/smith/isabelle";
1.241 -%gif_path := "/home/smith/isabelle/Tools";
1.242 -%init_html();
1.243 -%\dots
1.244 -%\end{ttbox}
1.245 -
1.246
1.247 \section{Terms}
1.248 \index{terms|bold}