--- a/doc-src/System/misc.tex Wed Oct 13 15:41:24 1999 +0200
+++ b/doc-src/System/misc.tex Wed Oct 13 19:39:19 1999 +0200
@@ -210,84 +210,6 @@
\texttt{make} invocation.
-\section{Running complete logics --- \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:
-\begin{ttbox}
-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)
- -i BOOL generate theory browsing information,
- i.e. HTML / graph data (default false)
- -r reset session path
- -s NAME override session NAME
-
- Build object-logic or run examples. Also creates browsing
- information (HTML etc.) according to settings.
-
- ISABELLE_USEDIR_OPTIONS=
-\end{ttbox}
-
-Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
-implicitly prefixed to \emph{any} \texttt{usedir} call. Since the
-\ttindex{IsaMakefile}s of all object-logics distributed with Isabelle
-just invoke \texttt{usedir} for the real work, one may control
-compilation options globally via above variable. In particular,
-generation of \rmindex{HTML} browsing information is enabled or
-disabled this way.
-
-
-\subsection*{Options}
-
-Basically, there are two different modes of operation: \emph{build
- mode} (enabled through the \texttt{-b} option) and \emph{example
- mode} (default).
-
-Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with input
-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.
-
-In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC}
-(typically just built before) and automatically runs \texttt{ROOT.ML} from
-within directory \texttt{NAME}. It assumes that file \texttt{ROOT.ML} in
-directory \texttt{NAME} contains appropriate {\ML} commands to run the desired
-examples.
-
-\medskip The \texttt{-i} option controls theory browsing data generation. It
-may be explicitly turned on or off --- 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.
-
-\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
-the examples of {\FOL} which is built upon {\Pure}.
-
-The current session's identifier is by default just the base name of
-the \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME}
-argument (in example mode). This may be overridden explicitely via the
-\texttt{-s} option.
-
-
-\subsection*{Examples}
-
-Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
-object-logics as a model for your own developements. For example, see
-\texttt{src/FOL/IsaMakefile}.
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"