diff -r 0a7c43c56092 -r 1a4ed2eb48f3 doc-src/System/misc.tex --- a/doc-src/System/misc.tex Mon Aug 16 22:08:23 1999 +0200 +++ b/doc-src/System/misc.tex Tue Aug 17 11:51:12 1999 +0200 @@ -223,6 +223,7 @@ -b build mode (output heap image, using current dir) -i BOOL generate theory browsing information, i.e. HTML / graph data (default false) + -m BOOL multi line output (default false) -r reset session path -s NAME override session NAME @@ -268,6 +269,11 @@ Thus user sessions may easily link to existing Isabelle libraries already present on the WWW. +\medskip Option \texttt{-m} controls multi-line mode of messages output as +\texttt{usedir} proceeds. By default, start and end of operation are printed +on a single line. One may specify \texttt{-m true} in case that printing of +partial lines causes any problems, e.g.\ when doing parallel make. + \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