# HG changeset patch # User wenzelm # Date 934989351 -7200 # Node ID b228e54a02c52f3a0c63141bd02ddec43496f8bf # Parent 745cfc8871e25f3fe87eac3c4dfea3403f3748f2 tuned; diff -r 745cfc8871e2 -r b228e54a02c5 doc-src/System/present.tex --- a/doc-src/System/present.tex Wed Aug 18 16:19:53 1999 +0200 +++ b/doc-src/System/present.tex Wed Aug 18 17:15:51 1999 +0200 @@ -6,45 +6,40 @@ \section{Generating theory browsing information} \label{sec:info} \index{theory browsing information|bold} -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. - -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. +Isabelle is able to generate theory browsing information, including HTML +documents that show a theory's definition, the theorems proved in its ML file +and the relationship with its ancestors and descendants. Besides the HTML +file that is generated for every theory, Isabelle stores links to all theories +in an index file. These indexes are 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 -can be comfortably displayed by a graph browser Java applet embedded -in the generated HTML pages. There is also a stand-alone version of -the graph browser which allows browsing theory graphs without having -to start a Web browser first. This version also includes features such -as generating {\sc PostScript} files, which are not available in the -applet version. The graph browser will be described later in this -chapter. +Isabelle also generates graph files that represent the theory hierarchy of a +logic. There is a graph browser Java applet embedded in the generated HTML +pages, and also a stand-alone application that allows browsing theory graphs +without having to start a WWW browser first. The latter version also includes +features such as generating {\sc PostScript} files, which are not available in +the applet version. See \S\ref{sec:browse} for further information. -\medskip To generate theory browsing information for logics that are -part of the Isabelle distribution, simply append ``\texttt{-i true}'' -to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic. -For example, to generate browsing information for {\FOL}, first add -something like this to your Isabelle settings file: +\medskip + +To generate theory browsing information for logics that are part of the +Isabelle distribution, simply append ``\texttt{-i true}'' to the +\settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic. For example, +in order to do this for {\FOL}, first add something like this to your Isabelle +settings file \begin{ttbox} ISABELLE_USEDIR_OPTIONS="-i true" \end{ttbox} -Then \texttt{cd} into the \texttt{src/FOL} directory of the Isabelle -distribution and do \texttt{isatool make} (or even \texttt{isatool - make all}). +and then change into the \texttt{src/FOL} directory of the Isabelle +distribution and run \texttt{isatool make}, or even \texttt{isatool make all}. + +\medskip -\medskip The directory in which to store theory browsing information -is determined by the \settdx{ISABELLE_BROWSER_INFO} setting. -The entry point to all logics is the {\tt index.html} file located in -the directory denoted by \texttt{ISABELLE_BROWSER_INFO}. - -A complete HTML version of all distributed Isabelle object-logics and -examples may be accessed on the WWW at: - +The theory browsing information is stored within the directory determined by +the \settdx{ISABELLE_BROWSER_INFO} setting. The \texttt{index.html} file +located there provides an entry point to all standard Isabelle logics. A +complete HTML version of all object-logics and examples of the Isabelle +distribution is available at \begin{center}\small \begin{tabular}{l} \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ @@ -52,45 +47,36 @@ \end{tabular} \end{center} -Of course, this is not necessarily consistent with your local version! +\medskip -\medskip -To present your own theories on the WWW, simply copy the whole -\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server. -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} - -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. - -You can add section headings to the list of theorems by using - -\begin{ttbox}\index{*use_dir} +The generated HTML document of any theory includes all theorems proved in the +corresponding {\ML} file, provided these have been stored properly via +\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm}, or +\ttindex{store_thm}. Section headings may be included in the presentation via +the {\ML} function +\begin{ttbox}\index{*section} 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. +\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. 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. +In order to present your own theories on the web, simply copy the whole +\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server, after generating +browser info like this: \begin{ttbox} -isatool usedir -i true - -P http://isabelle.in.tum.de/library/ HOL my_theories +isatool usedir -i true HOL Foobar \end{ttbox} +This assumes that directory \texttt{Foobar} contains some \texttt{ROOT.ML} +file to load all your theories, and {\HOL} is your parent logic image. +Ideally, theory browser information would have been generated for {\HOL} +already. + +Alternatively, one may specify an external link to an existing body of HTML +data by giving \texttt{usedir} a \texttt{-P} option like this: +\begin{ttbox} +isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foobar +\end{ttbox} + \section{Browsing theory graphs} \label{sec:browse} \index{theory graph browser|bold} diff -r 745cfc8871e2 -r b228e54a02c5 doc-src/System/system.tex --- a/doc-src/System/system.tex Wed Aug 18 16:19:53 1999 +0200 +++ b/doc-src/System/system.tex Wed Aug 18 17:15:51 1999 +0200 @@ -7,9 +7,7 @@ \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual} -\author{{\em Markus Wenzel}\/\thanks{Section~\protect\ref{sec:info} was - written by Carsten Clasohm. Section~\protect\ref{sec:browse} was - written by Stefan Berghofer.} \\ +\author{\emph{Markus Wenzel} and \emph{Stefan Berghofer} \\ TU M\"unchen} \makeindex