--- a/doc-src/System/present.tex Tue Aug 07 20:19:52 2007 +0200
+++ b/doc-src/System/present.tex Tue Aug 07 20:19:54 2007 +0200
@@ -361,7 +361,9 @@
Options are:
-C BOOL copy existing document directory to -D PATH (default true)
-D PATH dump generated document sources into PATH
+ -M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
+ -T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
-c BOOL tell ML system to compress output image (default true)
@@ -460,6 +462,17 @@
\medskip The \texttt{-v} option causes additional information to be printed
while running the session, notably the location of prepared documents.
+\medskip The \texttt{-M} option specifies the maximum number of
+parallel threads used for processing independent theory files
+(multithreading only works on suitable ML platforms). When tuning the
+performance of large Isabelle sessions, the number of actual CPU cores
+of the underlying hardware is a good starting point for option
+\texttt{-M}. The \texttt{-T} option determines the level of detail in
+tracing output concerning the internal locking and scheduling in
+multithreaded operation. This may be helpful in isolating performance
+bottle-necks, e.g.\ due to excessive wait states when locking critical
+code sections.
+
\medskip Any \texttt{usedir} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend on
others. For example, consider \texttt{Pure/FOL/ex}, which refers to the