# HG changeset patch
# User wenzelm
# Date 1186510794 -7200
# Node ID 9229d09363c0628cc0c39ee96303a6764191845b
# Parent  9620a57a5a579c17c0ffd502250aeae7ce95fa91
usedir: added options -M -T for multithreading;

diff -r 9620a57a5a57 -r 9229d09363c0 doc-src/System/present.tex
--- 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