446 -D PATH dump generated document sources into PATH |
446 -D PATH dump generated document sources into PATH |
447 -M MAX multithreading: maximum number of worker threads (default 1) |
447 -M MAX multithreading: maximum number of worker threads (default 1) |
448 -P PATH set path for remote theory browsing information |
448 -P PATH set path for remote theory browsing information |
449 -Q INT set threshold for sub-proof parallelization (default 50) |
449 -Q INT set threshold for sub-proof parallelization (default 50) |
450 -T LEVEL multithreading: trace level (default 0) |
450 -T LEVEL multithreading: trace level (default 0) |
451 -V VERSION declare alternative document VERSION |
451 -V VARIANT declare alternative document VARIANT |
452 -b build mode (output heap image, using current dir) |
452 -b build mode (output heap image, using current dir) |
453 -d FORMAT build document as FORMAT (default false) |
453 -d FORMAT build document as FORMAT (default false) |
454 -f NAME use ML file NAME (default ROOT.ML) |
454 -f NAME use ML file NAME (default ROOT.ML) |
455 -g BOOL generate session graph image for document (default false) |
455 -g BOOL generate session graph image for document (default false) |
456 -i BOOL generate theory browser information (default false) |
456 -i BOOL generate theory browser information (default false) |
521 session has to provide a properly setup @{verbatim document} |
521 session has to provide a properly setup @{verbatim document} |
522 directory. See \secref{sec:tool-document} and |
522 directory. See \secref{sec:tool-document} and |
523 \secref{sec:tool-latex} for more details. |
523 \secref{sec:tool-latex} for more details. |
524 |
524 |
525 \medskip The @{verbatim "-V"} option declares alternative document |
525 \medskip The @{verbatim "-V"} option declares alternative document |
526 versions, consisting of name/tags pairs (cf.\ options @{verbatim |
526 variants, consisting of name/tags pairs (cf.\ options @{verbatim |
527 "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool). The |
527 "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool). The |
528 standard document is equivalent to ``@{verbatim |
528 standard document is equivalent to ``@{verbatim |
529 "document=theory,proof,ML"}'', which means that all theory begin/end |
529 "document=theory,proof,ML"}'', which means that all theory begin/end |
530 commands, proof body texts, and ML code will be presented |
530 commands, proof body texts, and ML code will be presented |
531 faithfully. An alternative version ``@{verbatim |
531 faithfully. An alternative variant ``@{verbatim |
532 "outline=/proof/ML"}'' would fold proof and ML parts, replacing the |
532 "outline=/proof/ML"}'' would fold proof and ML parts, replacing the |
533 original text by a short place-holder. The form ``@{text |
533 original text by a short place-holder. The form ``@{text |
534 name}@{verbatim "=-"},'' means to remove document @{text name} from |
534 name}@{verbatim "=-"},'' means to remove document @{text name} from |
535 the list of versions to be processed. Any number of @{verbatim |
535 the list of variants to be processed. Any number of @{verbatim |
536 "-V"} options may be given; later declarations have precedence over |
536 "-V"} options may be given; later declarations have precedence over |
537 earlier ones. |
537 earlier ones. |
538 |
538 |
539 \medskip The @{verbatim "-g"} option produces images of the theory |
539 \medskip The @{verbatim "-g"} option produces images of the theory |
540 dependency graph (cf.\ \secref{sec:browse}) for inclusion in the |
540 dependency graph (cf.\ \secref{sec:browse}) for inclusion in the |