tuned;
authorwenzelm
Wed Aug 18 17:15:51 1999 +0200 (1999-08-18)
changeset 7258b228e54a02c5
parent 7257 745cfc8871e2
child 7259 e75aa311788c
tuned;
doc-src/System/present.tex
doc-src/System/system.tex
     1.1 --- a/doc-src/System/present.tex	Wed Aug 18 16:19:53 1999 +0200
     1.2 +++ b/doc-src/System/present.tex	Wed Aug 18 17:15:51 1999 +0200
     1.3 @@ -6,45 +6,40 @@
     1.4  \section{Generating theory browsing information} \label{sec:info}
     1.5  \index{theory browsing information|bold}
     1.6  
     1.7 -Isabelle is able to generate theory browsing information, such as HTML
     1.8 -documents that show a theory's definition, the theorems proved in its
     1.9 -ML file and the relationship with its ancestors and descendants.
    1.10 -
    1.11 -Besides the HTML file that is generated for every theory, Isabelle
    1.12 -stores links to all theories in an index file. These indexes are
    1.13 -themself linked with other indexes to represent the hierarchic
    1.14 -structure of Isabelle's logics.
    1.15 +Isabelle is able to generate theory browsing information, including HTML
    1.16 +documents that show a theory's definition, the theorems proved in its ML file
    1.17 +and the relationship with its ancestors and descendants.  Besides the HTML
    1.18 +file that is generated for every theory, Isabelle stores links to all theories
    1.19 +in an index file. These indexes are linked with other indexes to represent the
    1.20 +hierarchic structure of Isabelle's logics.
    1.21  
    1.22 -In addition to the HTML files, Isabelle also generates \emph{graph}
    1.23 -files that represent the theory hierarchy of a logic.  These graphs
    1.24 -can be comfortably displayed by a graph browser Java applet embedded
    1.25 -in the generated HTML pages. There is also a stand-alone version of
    1.26 -the graph browser which allows browsing theory graphs without having
    1.27 -to start a Web browser first. This version also includes features such
    1.28 -as generating {\sc PostScript} files, which are not available in the
    1.29 -applet version. The graph browser will be described later in this
    1.30 -chapter.
    1.31 +Isabelle also generates graph files that represent the theory hierarchy of a
    1.32 +logic.  There is a graph browser Java applet embedded in the generated HTML
    1.33 +pages, and also a stand-alone application that allows browsing theory graphs
    1.34 +without having to start a WWW browser first.  The latter version also includes
    1.35 +features such as generating {\sc PostScript} files, which are not available in
    1.36 +the applet version.  See \S\ref{sec:browse} for further information.
    1.37  
    1.38 -\medskip To generate theory browsing information for logics that are
    1.39 -part of the Isabelle distribution, simply append ``\texttt{-i true}''
    1.40 -to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic.
    1.41 -For example, to generate browsing information for {\FOL}, first add
    1.42 -something like this to your Isabelle settings file:
    1.43 +\medskip
    1.44 +
    1.45 +To generate theory browsing information for logics that are part of the
    1.46 +Isabelle distribution, simply append ``\texttt{-i true}'' to the
    1.47 +\settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic.  For example,
    1.48 +in order to do this for {\FOL}, first add something like this to your Isabelle
    1.49 +settings file
    1.50  \begin{ttbox}
    1.51  ISABELLE_USEDIR_OPTIONS="-i true"
    1.52  \end{ttbox}
    1.53 -Then \texttt{cd} into the \texttt{src/FOL} directory of the Isabelle
    1.54 -distribution and do \texttt{isatool make} (or even \texttt{isatool
    1.55 -  make all}).
    1.56 +and then change into the \texttt{src/FOL} directory of the Isabelle
    1.57 +distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
    1.58 +
    1.59 +\medskip
    1.60  
    1.61 -\medskip The directory in which to store theory browsing information
    1.62 -is determined by the \settdx{ISABELLE_BROWSER_INFO} setting.
    1.63 -The entry point to all logics is the {\tt index.html} file located in
    1.64 -the directory denoted by \texttt{ISABELLE_BROWSER_INFO}.
    1.65 -
    1.66 -A complete HTML version of all distributed Isabelle object-logics and
    1.67 -examples may be accessed on the WWW at:
    1.68 -
    1.69 +The theory browsing information is stored within the directory determined by
    1.70 +the \settdx{ISABELLE_BROWSER_INFO} setting.  The \texttt{index.html} file
    1.71 +located there provides an entry point to all standard Isabelle logics.  A
    1.72 +complete HTML version of all object-logics and examples of the Isabelle
    1.73 +distribution is available at
    1.74  \begin{center}\small
    1.75    \begin{tabular}{l}
    1.76      \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
    1.77 @@ -52,45 +47,36 @@
    1.78    \end{tabular}
    1.79  \end{center}
    1.80  
    1.81 -Of course, this is not necessarily consistent with your local version!
    1.82 +\medskip
    1.83  
    1.84 -\medskip
    1.85 -To present your own theories on the WWW, simply copy the whole
    1.86 -\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server.
    1.87 -When running your theories with the \texttt{usedir} utility, you can
    1.88 -generate browsing information by specifying the option \texttt{-i true}
    1.89 -on the command line, e.g.
    1.90 -\begin{ttbox}
    1.91 -isatool usedir -i true HOL my_theories
    1.92 -\end{ttbox}
    1.93 -
    1.94 -The generated HTML files contain all theorems that were
    1.95 -proved in the theories' \ML{} files with {\tt qed}, {\tt qed_goal} and
    1.96 -{\tt qed_goalw}, or stored with {\tt bind_thm} and {\tt store_thm}.
    1.97 -Additionally, there is a hypertext link to the whole \ML{} file.
    1.98 -
    1.99 -You can add section headings to the list of theorems by using
   1.100 -
   1.101 -\begin{ttbox}\index{*use_dir}
   1.102 +The generated HTML document of any theory includes all theorems proved in the
   1.103 +corresponding {\ML} file, provided these have been stored properly via
   1.104 +\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm}, or
   1.105 +\ttindex{store_thm}.  Section headings may be included in the presentation via
   1.106 +the {\ML} function
   1.107 +\begin{ttbox}\index{*section}
   1.108  section: string -> unit
   1.109  \end{ttbox}
   1.110  
   1.111 -in a theory's ML file, which converts a plain string to a HTML heading
   1.112 -and inserts it before the next theorem proved or stored with one of
   1.113 -the above functions.
   1.114 +\medskip
   1.115  
   1.116 -As some of Isabelle's logics are based on others (e.g. {\tt ZF}
   1.117 -on {\tt FOL}) and because the HTML files list a theory's
   1.118 -ancestors, you should not make HTML files for a logic if the HTML
   1.119 -files for the base logic do not exist. Otherwise some of the hypertext
   1.120 -links might point to non-existing documents. If the HTML files for the
   1.121 -base logic are located in a directory other than \texttt{ISABELLE_BROWSER_INFO}
   1.122 -or on a WWW server, you have to specify this directory or URL via
   1.123 -the \texttt{-P} option, e.g.
   1.124 +In order to present your own theories on the web, simply copy the whole
   1.125 +\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server, after generating
   1.126 +browser info like this:
   1.127  \begin{ttbox}
   1.128 -isatool usedir -i true
   1.129 -  -P http://isabelle.in.tum.de/library/ HOL my_theories
   1.130 +isatool usedir -i true HOL Foobar
   1.131  \end{ttbox}
   1.132 +This assumes that directory \texttt{Foobar} contains some \texttt{ROOT.ML}
   1.133 +file to load all your theories, and {\HOL} is your parent logic image.
   1.134 +Ideally, theory browser information would have been generated for {\HOL}
   1.135 +already.
   1.136 +
   1.137 +Alternatively, one may specify an external link to an existing body of HTML
   1.138 +data by giving \texttt{usedir} a \texttt{-P} option like this:
   1.139 +\begin{ttbox}
   1.140 +isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foobar
   1.141 +\end{ttbox}
   1.142 +
   1.143  
   1.144  \section{Browsing theory graphs} \label{sec:browse}
   1.145  \index{theory graph browser|bold} 
     2.1 --- a/doc-src/System/system.tex	Wed Aug 18 16:19:53 1999 +0200
     2.2 +++ b/doc-src/System/system.tex	Wed Aug 18 17:15:51 1999 +0200
     2.3 @@ -7,9 +7,7 @@
     2.4  
     2.5  \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
     2.6  
     2.7 -\author{{\em Markus Wenzel}\/\thanks{Section~\protect\ref{sec:info} was
     2.8 -    written by Carsten Clasohm.  Section~\protect\ref{sec:browse} was
     2.9 -    written by Stefan Berghofer.} \\
    2.10 +\author{\emph{Markus Wenzel} and \emph{Stefan Berghofer} \\
    2.11    TU M\"unchen}
    2.12  
    2.13  \makeindex