usedir -D: update styles as well;
Fri, 24 Mar 2000 13:48:31 +0100
changeset 8567 e6d46b03f2cb
parent 8566 30261b1917b5
child 8568 b18540435f26
usedir -D: update styles as well;
--- a/doc-src/System/present.tex	Fri Mar 24 13:48:01 2000 +0100
+++ b/doc-src/System/present.tex	Fri Mar 24 13:48:31 2000 +0100
@@ -327,7 +327,7 @@
   Options are:
     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
-                 ps.gz, pdf, bbl, png
+                 ps.gz, pdf, bbl, png, sty
   Run LaTeX (and related tools) on FILE (default root.tex),
   producing the specified output format.
@@ -338,6 +338,12 @@
 The actual commands are determined from the settings environment
 (\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
+The \texttt{sty} output format causes the Isabelle style files to be updated
+from the distribution.  This is useful in special situations where the
+document sources are to be processed another time by separate tools (cf.\ 
+option \texttt{-D} of the \texttt{usedir} utility, see
 It is important to note that the {\LaTeX} inputs file space has to be properly
 setup to include the Isabelle styles.  Usually, this may be done by modifying
 the \settdx{TEXINPUTS} variable in settings like this:
@@ -484,7 +490,8 @@
 directory.  For example, \texttt{-D document} would leave a copy of the
 {\LaTeX} sources in the actual document directory.  Thus the Isabelle
 \texttt{document} or \texttt{latex} tools may be run later, facilitating much
-easier debugging of {\LaTeX} errors, for example.
+easier debugging of {\LaTeX} errors, for example.  Note that a copy of the
+Isabelle style files will be placed in \texttt{PATH} as well.
 \medskip Any \texttt{usedir} session is named by some \emph{session
   identifier}. These accumulate, documenting the way sessions depend on