1.1 --- a/doc-src/System/present.tex Wed Jan 02 16:17:49 2008 +0100
1.2 +++ b/doc-src/System/present.tex Wed Jan 02 16:32:52 2008 +0100
1.3 @@ -469,14 +469,14 @@
1.4
1.5 \medskip The \texttt{-M} option specifies the maximum number of
1.6 parallel threads used for processing independent theory files
1.7 -(multithreading only works on suitable ML platforms). When tuning the
1.8 -performance of large Isabelle sessions, the number of actual CPU cores
1.9 -of the underlying hardware is a good starting point for option
1.10 -\texttt{-M}. The \texttt{-T} option determines the level of detail in
1.11 -tracing output concerning the internal locking and scheduling in
1.12 -multithreaded operation. This may be helpful in isolating performance
1.13 -bottle-necks, e.g.\ due to excessive wait states when locking critical
1.14 -code sections.
1.15 +(multithreading only works on suitable ML platforms). The special
1.16 +value of ``\texttt{0}'' or ``\texttt{max}'' refers to the number of
1.17 +actual CPU cores of the underlying machine, which is a good starting
1.18 +point for optimal performance tuning. The \texttt{-T} option
1.19 +determines the level of detail in tracing output concerning the
1.20 +internal locking and scheduling in multithreaded operation. This may
1.21 +be helpful in isolating performance bottle-necks, e.g.\ due to
1.22 +excessive wait states when locking critical code sections.
1.23
1.24 \medskip Any \texttt{usedir} session is named by some \emph{session
1.25 identifier}. These accumulate, documenting the way sessions depend on
2.1 --- a/lib/Tools/usedir Wed Jan 02 16:17:49 2008 +0100
2.2 +++ b/lib/Tools/usedir Wed Jan 02 16:32:52 2008 +0100
2.3 @@ -96,8 +96,12 @@
2.4 DUMP="$OPTARG"
2.5 ;;
2.6 M)
2.7 - check_number "$OPTARG"
2.8 - MAXTHREADS="$OPTARG"
2.9 + if [ "$OPTARG" = max ]; then
2.10 + MAXTHREADS=0
2.11 + else
2.12 + check_number "$OPTARG"
2.13 + MAXTHREADS="$OPTARG"
2.14 + fi
2.15 ;;
2.16 P)
2.17 RPATH="$OPTARG"