# HG changeset patch # User wenzelm # Date 863630841 -7200 # Node ID 445555a7b714ff498366538d916721dfcd84cf2f # Parent 8f8c88dcd728d9dc5e4999f9e8c013dea9f0a226 preliminary! diff -r 8f8c88dcd728 -r 445555a7b714 doc-src/System/basics.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/basics.tex Wed May 14 19:27:21 1997 +0200 @@ -0,0 +1,229 @@ + +% $Id$ + +\chapter{Basic concepts} + +The \emph{Isabelle System Manual} describes Isabelle together with its +related tools and user interfaces --- as seen from an outside +(operating system oriented) view. On the other hand, see +\emph{Isabelle Reference} for all internal {\ML} level user commands. + +\medskip The Isabelle system level environment is based on a few +generic concepts that are simple, but non-trivial: +\begin{itemize} +\item The \emph{Isabelle settings mechanism}, which provides + environment values to all Isabelle programs (including tools and + user interfaces). +\item \emph{Isabelle proper} (\ttindex{isabelle}), which runs logic + sessions, both interactively or in batch mode. In particular, + \texttt{isabelle} abstracts over the invocation of the actual {\ML} + system to be used. +\item The \emph{Isabelle tools wrapper} (\ttindex{isatool}), which + provides a generic startup platform for miscellaneous utilities. + Thus tools automatically benefit from the settings mechanism. + Furthermore, the shell's search path is kept clean from many small + programs. +\item The \emph{Isabelle interface wrapper} + (\ttindex{Isabelle}\footnote{Note the capital \texttt{I}!}), which + provides some abstraction over the actual user interface to be used + (this may include third-party ones). +\end{itemize} + +\medskip The beginning user would probably just run one of the +interfaces (by invoking the capital \texttt{Isabelle}), and maybe some +basic other tools like \texttt{doc} (see \S\ref{sec:tool-doc}). This +assumes that the system has already been installed properly, of +course.\footnote{In case you have to do this yourself from scratch, + see the \ttindex{INSTALL} file in the top-level directory of the + distribution. The information provided there should be sufficient as + a start.} + + +\section{Isabelle settings} \label{sec:settings} + +The Isabelle system heavily depends on the \emph{settings + mechanism}\indexbold{settings}. Basically, this is just a collection +of environment variables, e.g.\ \texttt{ISABELLE_HOME}, +\texttt{ML_SYSTEM}, \texttt{ML_HOME}. These variables are \emph{not} +intended to be set directly from the shell! + +Isabelle employs a somewhat more sophisticated scheme of +\emph{settings files} --- one for site-wide defaults, another for +optional user-specific modifications. With all configuration +variables in only one or two places, this is considered much more +maintainable and user-friendly than ordinary shell environment +variables. + +In particular, we avoid the typical situation where prospective users +of a software package are told to put this and that in their shell +startup scripts. Isabelle requires none such administrative chores of +its end-users --- the executables can be run straight away. Usually, +users would want to put the Isabelle \texttt{bin} directory into their +shell's search path, of course. + + +\subsection{Building the environment} + +The environment that all Isabelle programs are run in is built as +follows: + +\begin{enumerate} +\item The special variable \ttindex{ISABELLE_HOME} is determined + automatically from the location of the binary that has been run + (e.g.\ \texttt{isabelle}). + + You should not try to set \texttt{ISABELLE_HOME} manually. Also note + that the Isabelle executables have to be run from their original + location in the distribution directory --- copying or linking them + somewhere else just won't work! + +\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a GNU + bash script with the variable auto-export option enabled. + + The file typically contains a rather long list of assigments + \texttt{FOO="bar"}, thus providing the site default settings. The + Isabelle distribution already contains a global settings file with + sensible defaults. When installing the system, only a few of these + have to be adapted (most likely \texttt{ML_SYSTEM} and friends). + +\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it + exists) is run the same way as the site default settings. The + variable \texttt{ISABELLE_HOME_USER} has already been set before --- + usually to \texttt{\~\relax/isabelle}. + + Thus individual users may override the site-wide defaults. See also + file \texttt{etc/user-settings.sample} in the distribution. + Typically, user settings are a few lines only, just containing the + assigments that are really required. One should definitely + \emph{not} start with a full copy the central + \texttt{\$ISABELLE_HOME/etc/settings}. This may cause severe + maintainance problems later, when the Isabelle installation is + updated or changed otherwise. + +\end{enumerate} + +Note that settings files are actually bash scripts. So one may use +complex shell commands, e.g.\ \texttt{if} or \texttt{case} statements +to set variables depending on the system architecture or other +environment variables. Such advanced features should be added only +with great care, though. In particular, external environment +references should be kept at a minimum. + +\medskip A few variables are somewhat: +\begin{itemize} +\item \ttindex{ISABELLE} and \ttindex{ISATOOL} are set automatically + to the absolute path names of the \texttt{isabelle} and + \texttt{isatool} executables, respectively. + +\item \ttindex{ISABELLE_PATH} and \ttindex{ISABELLE_OUTPUT} will have + the {\ML} system identifier (as specified by \texttt{ML_SYSTEM}) + automatically appended to their values. +\end{itemize} + +\medskip The Isabelle settings scheme is basically quite simple, but +non-trivial. For debugging purposes, the generated environment may be +inspected with the \texttt{getenv} Isabelle tool, see +\S\ref{sec:tool-getenv}. + + +\subsection{Common variables} + +Below is a reference of common Isabelle settings variables. The list +is somewhat open-ended, in particular, third-party utilities or +interfaces may add their own selection. + +\begin{ttdescription} +\item[FIXME] FIXME +\end{ttdescription} + + +\section{Isabelle proper --- \texttt{isabelle}} + +The \ttindex{isabelle} executable runs logic sessions --- either +interactively or in batch mode. It provides an abstraction over the +underlying {\ML} system, and over the actual heap file locations. The usage is: +\begin{ttbox} +Usage: isabelle [OPTIONS] [INPUT] [OUTPUT] + + Options are: + -e MLTEXT pass MLTEXT to the ML session + -m MODE add print mode for output + -q non-interactive session + -r open heap file read-only + + INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps. + These are either names to be searched in the Isabelle path, or actual + file names (then containing at least one /). + If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system. +\end{ttbox} +Input files without path specifications are looked up in the +\texttt{ISABELLE_PATH} setting, which may consist of multiple +components separated by colons --- these are tried in the given order. +Short output names are relative to the directory specified by +\texttt{ISABELLE_OUTPUT} setting. In any case, actual file locations +can be given by including at least one \texttt{/} (use \texttt{./} to +refer to the current directory). + +If the input heap file is not writable, or the \texttt{-r} option is +given explicitely, the session will be read-only. That is, the {\ML} +world cannot be committed back into the logic image. A writable +session enables commits into either the input file, or into an +alternative output heap file which may be given as the second +argument. + +The read-write state of sessions is determined at startup only, it +cannot be changed intermediately. Also note that heap images may +require considerable amounts of disk space. Users are responsible +themselves to dispose no longer needed heap files. + + +\subsection*{Options} + +Using \texttt{-e} one may pass {\ML} code to the Isabelle session from +the command line. Multiple \texttt{-e}'s are evaluated in the given +order. + +The \texttt{-m} option addes print mode identifiers to be made active +for this session. Typically this is used by some user interface to +enable output of mathematical symbols from a special screen font, for +example (see also \S\ref{sec:fonts} about fonts and the \emph{Isabelle + Reference Manual} about print modes in general). + +Isabelle normally enters an interactice {\ML} top-level loop (after +processing the \texttt{-e} texts). The \texttt{-q} option inhibits +this, providing a pure batch mode facility. + + +\subsection*{Examples} + +Run an interactive session of the default object-logic: +\begin{ttbox} +isabelle +\end{ttbox} +Usually, this refers to one of the standard logic images, which are +read-only by default. + +Run a writable session, based on \texttt{FOL}, but output to +\texttt{Foo} (in the directory specified by the +\texttt{ISABELLE_OUTPUT} setting): +\begin{ttbox} +isabelle FOL Foo +\end{ttbox} +Ending this session normally (e.g.\ by typing control-D), dumps the +whole {\ML} system state into \texttt{Foo}. Be prepared for several +megabytes! + +The \texttt{Foo} session may be continued (writably!) at exactly the +same point as follows: +\begin{ttbox} +isabelle Foo +\end{ttbox} + +\medskip This is a simple batch mode example, printing a certain +theorem of \texttt{FOL}: +\begin{ttbox} +isabelle -e "prth allE;" -q -r FOL +\end{ttbox} +Note that the output text will be usually interspered with some +garbage produced by the {\ML} compiler. + diff -r 8f8c88dcd728 -r 445555a7b714 doc-src/System/fonts.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/fonts.tex Wed May 14 19:27:21 1997 +0200 @@ -0,0 +1,21 @@ + +\chapter{Fonts and character encodings} + +\section{ --- \texttt{isatool installfonts}} + +\begin{ttbox} +Usage: isatool installfonts + + Install the isabelle fonts into your X11 server. + (May be savely called repeatedly.) +\end{ttbox} + + +\section{ --- \texttt{isatool symbolinput}} + + +%FIXME not yet +%\section{ --- \texttt{isatool showsymbols}} +% +%\begin{ttbox} +%\end{ttbox} diff -r 8f8c88dcd728 -r 445555a7b714 doc-src/System/html.tex --- a/doc-src/System/html.tex Wed May 14 18:42:09 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,211 +0,0 @@ -\chapter{Generating HTML documents} \label{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} diff -r 8f8c88dcd728 -r 445555a7b714 doc-src/System/misc.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/misc.tex Wed May 14 19:27:21 1997 +0200 @@ -0,0 +1,111 @@ + +% $Id$ + +\chapter{Miscellaneous tools} + + +\section{Inspecting the settings environment -- \texttt{isatool getenv}} +\label{sec:tool-getenv} + +The Isabelle settings environment --- as provided by the site-default +and user-specific settings files --- can be inspected with the +\tooldx{getenv} utility: +\begin{ttbox} +Usage: isatool getenv [OPTIONS] [VARNAMES ...] + + Options are: + -a display complete environment + -b print values only (doesn't work for -a) + + Get value of VARNAMES from the Isabelle settings. +\end{ttbox} + +With the \texttt{-a} option, one may inspect the full process +environment that Isabelle related programs are run in. This usually +contains much more variables than are actually Isabelle settings. + +Unless the \texttt{-b} option is given, the output is a list of lines +of the form $varname\mathtt{=}value$. + + +\subsection*{Examples} + +Get the {\ML} system identifier and the location where the compiler +binaries are supposed to be installed as follows: +\begin{ttbox} +isatool getenv ML_SYSTEM ML_HOME +{\out ML_HOME=/usr/local/sml109.27/bin} +{\out ML_SYSTEM=smlnj-1.09} +\end{ttbox} + +This one peeks at the search path that \texttt{isabelle} uses to +locate logic images: +\begin{ttbox} +isatool getenv -b ISABELLE_PATH +{\out /home/mmw/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09} +\end{ttbox} +We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=} +prefix. The value above is what became of the following assignment in +the default settings file: +\begin{ttbox} +ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps +\end{ttbox} +Note how \texttt{\$ML_SYSTEM} got appended automatically to each path +component. This is a special feature of \texttt{ISABELLE_PATH} (and +also of \texttt{ISABELLE_OUTPUT}). + +\section{Get logic images --- \texttt{isatool findlogics}} + +\begin{ttbox} +Usage: isatool findlogics + + Collect heap file names from ISABELLE_PATH. +\end{ttbox} + +\section{Isabelle's version of make --- \texttt{isatool make}} + +\begin{ttbox} +Usage: isatool make [ARGS ...] + + Compiles logic in current directory using IsaMakefile. + ARGS are directly passed to the system make program. +\end{ttbox} + + +\section{ --- \texttt{isatool usedir}} + +\begin{ttbox} +Usage: isatool usedir LOGIC NAME + + Options are: + -b build mode (output heap image, use dir ".") + -g BOOL generate theory graph data (default false) + -h BOOL generate theory HTML data (default false) + -s NAME override session NAME + + Build object-logic or run examples. Also creates browsing + information (HTML etc.) according to settings. +\end{ttbox} + + +\section{ --- \texttt{isatool doc}} + +\begin{ttbox} +Usage: isatool doc [DOC] + + View Isabelle documentation DOC, or show list of available documents. +\end{ttbox} + + +\section{ --- \texttt{isatool expandshort}} + +\begin{ttbox} +Usage: expandshort [FILES ...] + + Expand shorthand goal commands in FILES. Also contracts uses of + resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on + 1-element lists; furthermore expands tabs, since they are now + forbidden in ML string constants. + + Renames old versions of FILES by appending "~~". +\end{ttbox} diff -r 8f8c88dcd728 -r 445555a7b714 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} diff -r 8f8c88dcd728 -r 445555a7b714 doc-src/System/system.ind --- a/doc-src/System/system.ind Wed May 14 18:42:09 1997 +0200 +++ b/doc-src/System/system.ind Wed May 14 19:27:21 1997 +0200 @@ -1,25 +1,42 @@ \begin{theindex} - \item browser, \bold{5} + \item browser, \bold{14} \indexspace - \item {\tt finish_html}, \bold{2} + \item {\tt finish_html}, \bold{11} + + \indexspace + + \item {\tt getenv} tool, 5 + + \indexspace + + \item HTML, \bold{10} \indexspace - \item HTML, \bold{1} - - \indexspace - - \item {\tt init_html}, \bold{2} + \item {\tt init_html}, \bold{11} + \item {\tt INSTALL}, 1 + \item {\tt ISABELLE}, 3 + \item {\tt Isabelle}, 1 + \item {\tt isabelle}, 1, 3 + \item {\tt ISABELLE_HOME}, 2 + \item {\tt ISABELLE_OUTPUT}, 3 + \item {\tt ISABELLE_PATH}, 3 + \item {\tt ISATOOL}, 3 + \item {\tt isatool}, 1 \indexspace - \item {\tt make_html}, \bold{2} + \item {\tt make_html}, \bold{11} \indexspace - \item {\tt use_dir}, 3 + \item settings, \bold{1} + + \indexspace + + \item {\tt use_dir}, 12 \end{theindex} diff -r 8f8c88dcd728 -r 445555a7b714 doc-src/System/system.tex --- a/doc-src/System/system.tex Wed May 14 18:42:09 1997 +0200 +++ b/doc-src/System/system.tex Wed May 14 19:27:21 1997 +0200 @@ -17,7 +17,7 @@ With Contributions by Tobias Nipkow and Markus Wenzel% \thanks{Chapter~\protect\ref{html} was written by Carsten Clasohm. Chapter~\protect\ref{browse} was written by Stefan - Berghofer. Some other parts are by Markus Wenzel.}} + Berghofer. Other parts are by Markus Wenzel.}} \makeindex @@ -35,7 +35,10 @@ %\include{introduction} -\include{html} +\include{basics} +\include{misc} +\include{fonts} +\include{present} \include{browse} %\begingroup