doc-src/System/present.tex

 Usage: usedir [OPTIONS] LOGIC NAME
 
   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)
     -d FORMAT    build document as FORMAT (default false)
     -f NAME      use ML file NAME (default ROOT.ML)

   Manual}~\cite{isabelle-ref}.
 
 \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
 examples of FOL, which in turn is built upon Pure.