diff -r 52fb3667f7df -r 01e6e05d208b doc-src/System/present.tex --- a/doc-src/System/present.tex Mon Oct 18 19:43:18 1999 +0200 +++ b/doc-src/System/present.tex Tue Oct 19 13:45:51 1999 +0200 @@ -324,7 +324,7 @@ -\section{Managing logic sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir} +\section{Managing Isabelle logic sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir} The \tooldx{usedir} utility builds object-logic images, or runs example sessions based on existing logics. Its usage is: @@ -332,7 +332,6 @@ Usage: usedir LOGIC NAME Options are: - -B build mode with THIS_IS_ISABELLE_BUILD indication -P PATH set path for remote theory browsing information -b build mode (output heap image, using current dir) -d FORMAT build document as FORMAT (default false) @@ -364,11 +363,7 @@ image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command line. This will be a batch session, running \texttt{ROOT.ML} from the current directory and then quitting. It is assumed that \texttt{ROOT.ML} contains all -{\ML} commands required to build the logic. The \texttt{-B} option is like -\texttt{-b}, but also indicates \texttt{THIS_IS_ISABELLE_BUILD=true} via the -process environment. This usually causes the \texttt{ISABELLE\_OUTPUT} and -\texttt{ISABELLE_BROWSER_INFO} settings to refer to some location within the -Isabelle distribution directory, rather than the user's home directory. +{\ML} commands required to build the logic. In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC} and automatically runs \texttt{ROOT.ML} from within directory \texttt{NAME}. @@ -405,7 +400,6 @@ object-logics as a model for your own developments. For example, see \texttt{src/FOL/IsaMakefile}. - %%% Local Variables: %%% mode: latex %%% TeX-master: "system"