# HG changeset patch
# User wenzelm
# Date 953902111 -3600
# Node ID e6d46b03f2cbe06c173d79078a5dacc7eec33747
# Parent  30261b1917b582895d79e282dd636adaabf265d8
usedir -D: update styles as well;

diff -r 30261b1917b5 -r e6d46b03f2cb doc-src/System/present.tex
--- 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
+\S\ref{sec:tool-usedir}).
+
 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