1.1 --- a/doc-src/System/Thy/Presentation.thy	Sun Jul 19 19:20:17 2009 +0200
     1.2 +++ b/doc-src/System/Thy/Presentation.thy	Sun Jul 19 19:24:04 2009 +0200
     1.3 @@ -451,7 +451,8 @@
     1.4      -g BOOL      generate session graph image for document (default false)
     1.5      -i BOOL      generate theory browser information (default false)
     1.6      -m MODE      add print mode for output
     1.7 -    -p LEVEL     set level of detail for proof objects
     1.8 +    -p LEVEL     set level of detail for proof objects (default 0)
     1.9 +    -q LEVEL     set level of parallel proof checking (default 1)
    1.10      -r           reset session path
    1.11      -s NAME      override session NAME
    1.12      -t BOOL      internal session timing (default false)
    1.13 @@ -564,6 +565,12 @@
    1.14    for internal proof objects, see also the \emph{Isabelle Reference
    1.15    Manual}~\cite{isabelle-ref}.
    1.16  
    1.17 +  \medskip The @{verbatim "-q"} option specifies the level of parallel
    1.18 +  proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
    1.19 +  proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
    1.20 +  The resulting speedup may vary, depending on the number of worker
    1.21 +  threads, granularity of proofs, and whether proof terms are enabled.
    1.22 +
    1.23    \medskip The @{verbatim "-t"} option produces a more detailed
    1.24    internal timing report of the session.
    1.25  
    1.26 @@ -583,13 +590,6 @@
    1.27    bottle-necks, e.g.\ due to excessive wait states when locking
    1.28    critical code sections.
    1.29  
    1.30 -  \medskip The @{verbatim "-Q"} option tells whether individual proofs
    1.31 -  should be checked in parallel; the default is @{verbatim true}.
    1.32 -  Note that fine-grained proof parallelism requires considerable
    1.33 -  amounts of extra memory, since full proof context information is
    1.34 -  maintained for each independent derivation thread, until checking is
    1.35 -  completed.
    1.36 -
    1.37    \medskip Any @{tool usedir} session is named by some \emph{session
    1.38    identifier}. These accumulate, documenting the way sessions depend
    1.39    on others. For example, consider @{verbatim "Pure/FOL/ex"}, which