--- 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"