doc-src/System/present.tex
changeset 13047 f27cc0a43feb
parent 13018 5164177cf0a6
child 14921 4ad751fa50c1
     1.1 --- a/doc-src/System/present.tex	Mon Mar 04 22:32:58 2002 +0100
     1.2 +++ b/doc-src/System/present.tex	Fri Mar 08 15:33:32 2002 +0100
     1.3 @@ -153,19 +153,16 @@
     1.4  When no filename is specified, the browser automatically changes to the
     1.5  directory \texttt{ISABELLE_BROWSER_INFO}.
     1.6  
     1.7 -\medskip The \texttt{-d} option cases the source file (!)\ to be deleted after
     1.8 -the browser terminates; this is mainly intended for detaching interactive
     1.9 -graph views from a running Isabelle session.
    1.10 +\medskip The \texttt{-d} option causes the source file (!)\ to be deleted
    1.11 +after the browser terminates; this is mainly intended for detaching
    1.12 +interactive graph views from a running Isabelle session.
    1.13  
    1.14  The \texttt{-o} option indicates batch-mode operation, with the output written
    1.15  to the indicated file; note that \texttt{pdf} produces an \texttt{eps} copy as
    1.16  well.
    1.17  
    1.18 -\medskip The applet version of the browser can be invoked by opening the {\tt
    1.19 -  index.html} file in the directory \texttt{ISABELLE_BROWSER_INFO} from your
    1.20 -Web browser and selecting the version ``including theory graph browser''.
    1.21 -There is also a link to the corresponding theory graph in every logic's {\tt
    1.22 -  index.html} file.
    1.23 +\medskip The applet version of the browser is part of the standard WWW theory
    1.24 +presentation, see the link ``theory dependencies'' within each session index.
    1.25  
    1.26  
    1.27  \subsection{Using the graph browser}
    1.28 @@ -282,8 +279,8 @@
    1.29  The \tooldx{mkdir} utility prepares Isabelle session source directories,
    1.30  including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML},
    1.31  and a \texttt{document} directory with a minimal \texttt{root.tex} that is
    1.32 -sufficient print all theories of the session (in the order of appearance); see
    1.33 -\S\ref{sec:tool-document} for further information on Isabelle document
    1.34 +sufficient to print all theories of the session (in the order of appearance);
    1.35 +see \S\ref{sec:tool-document} for further information on Isabelle document
    1.36  preparation.  The usage of \texttt{isatool mkdir} is:
    1.37  \begin{ttbox}
    1.38  Usage: mkdir [OPTIONS] [LOGIC] NAME
    1.39 @@ -343,8 +340,8 @@
    1.40  \texttt{ROOT.ML} should be edited to load all required theories.  Invoking
    1.41  \texttt{isatool make} again would run the whole session, generating browser
    1.42  information and the document automatically.  The \texttt{IsaMakefile} is
    1.43 -typically tuned manually later, e.g.\ adding actual source dependencies, or
    1.44 -changing the options passed to \texttt{usedir}.
    1.45 +typically tuned manually later, e.g.\ adding source dependencies, or changing
    1.46 +the options passed to \texttt{usedir}.
    1.47  
    1.48  \medskip Large projects may demand further sessions, potentially with separate
    1.49  logic images being created.  This usually requires manual editing of the
    1.50 @@ -428,10 +425,10 @@
    1.51  The \texttt{-g} option produces images of the theory dependency graph (cf.\ 
    1.52  \S\ref{sec:browse}) for inclusion in the generated document, both as
    1.53  \texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time.
    1.54 -In order to make this appear the final {\LaTeX} document one would typically
    1.55 -say \verb,\includegraphics{session_graph}, in the \texttt{document/root.tex}
    1.56 -file.  (Omitting the file-name extension enables {\LaTeX} to select to correct
    1.57 -version, either for the DVI or PDF output path.)
    1.58 +To include this in the final {\LaTeX} document one could say
    1.59 +\verb,\includegraphics{session_graph}, in \texttt{document/root.tex} (omitting
    1.60 +the file-name extension enables {\LaTeX} to select to correct version, either
    1.61 +for the DVI or PDF output path).
    1.62  
    1.63  \medskip The \texttt{-D} option causes the generated document sources
    1.64  (including the user's template of \texttt{document/root.tex} etc.) to be
    1.65 @@ -448,7 +445,7 @@
    1.66    Manual}~\cite{isabelle-ref}.
    1.67  
    1.68  \medskip The \texttt{-v} option causes additional information to be printed
    1.69 -during while running the session, notably the location of prepared documents.
    1.70 +while running the session, notably the location of prepared documents.
    1.71  
    1.72  \medskip Any \texttt{usedir} session is named by some \emph{session
    1.73    identifier}. These accumulate, documenting the way sessions depend on
    1.74 @@ -518,8 +515,8 @@
    1.75  
    1.76  The {\LaTeX} versions of the theories require some macros defined in
    1.77  \texttt{isabelle.sty} as distributed with Isabelle.  Doing
    1.78 -\verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
    1.79 -the underlying Isabelle \texttt{latex} utility already includes an appropriate
    1.80 +\verb,\usepackage{isabelle}, in \texttt{root.tex} should be fine; the
    1.81 +underlying Isabelle \texttt{latex} utility already includes an appropriate
    1.82  {\TeX} inputs path.
    1.83  
    1.84  If the text contains any references to Isabelle symbols (such as