# HG changeset patch # User wenzelm # Date 975696042 -3600 # Node ID 42f41f966db4ae3b7b7592006b06ea783811e417 # Parent e52adaeac996c03f6a38cf05d3bd96b061eacf90 usedir: -m option; diff -r e52adaeac996 -r 42f41f966db4 doc-src/System/present.tex --- a/doc-src/System/present.tex Fri Dec 01 19:40:18 2000 +0100 +++ b/doc-src/System/present.tex Fri Dec 01 19:40:42 2000 +0100 @@ -439,8 +439,8 @@ -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) - -i BOOL generate theory browsing information, - i.e. HTML / graph data (default false) + -i BOOL generate theory browser information (default false) + -m MODE add print mode for output -r reset session path -s NAME override session NAME @@ -476,10 +476,14 @@ \medskip The \texttt{-i} option controls theory browser data generation. It may be explicitly turned on or off --- as usual, the last occurrence of -\texttt{-i} on the command line wins. The \texttt{-P} option specifies a path -(or actual URL) to be prefixed to any \emph{non-local} reference of existing -theories. Thus user sessions may easily link to existing Isabelle libraries -already present on the WWW. +\texttt{-i} on the command line wins. + +The \texttt{-P} option specifies a path (or actual URL) to be prefixed to any +\emph{non-local} reference of existing theories. Thus user sessions may +easily link to existing Isabelle libraries already present on the WWW. + +The \texttt{-m} options specifies additional print modes to be activated +temporarily while the session is processed. \medskip The \texttt{-d} option controls document preparation. Valid arguments are \texttt{false} (do not prepare any document; this is default),