# HG changeset patch # User berghofe # Date 934983645 -7200 # Node ID 35de2117b5dd167fd83e2b7781ca38f6c6cb92f6 # Parent a4bd83b25d2320ff5c4a555d7fc555e50f83b001 Modified section about generation of theory browsing information. Documented new -P option. diff -r a4bd83b25d23 -r 35de2117b5dd doc-src/System/present.tex --- 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}