Updated usage information for tool "usedir".
--- a/doc-src/System/misc.tex Tue Sep 30 17:28:54 1997 +0200
+++ b/doc-src/System/misc.tex Tue Sep 30 17:29:32 1997 +0200
@@ -140,14 +140,13 @@
The \tooldx{usedir} utility builds object-logic images, or runs
example sessions based on existing logics. Its usage is:
-%FIXME
-% -g BOOL generate theory graph data (default false)
\begin{ttbox}
-Usage: isatool usedir LOGIC NAME
+Usage: usedir LOGIC NAME
Options are:
-b build mode (output heap image, use dir ".")
- -h BOOL generate theory HTML data (default false)
+ -i BOOL generate theory browsing information,
+ i.e. HTML / graph data (default false)
-s NAME override session NAME
Build object-logic or run examples. Also creates browsing
@@ -182,9 +181,9 @@
\texttt{ROOT.ML} in directory \texttt{NAME} contains appropriate {\ML}
commands to run the desired examples.
-\medskip The \texttt{-h} option controls HTML browsing data
+\medskip The \texttt{-i} option controls theory browsing data
generation. It may be explicitely turned on or off --- the last
-occurrence of some \texttt{-h} on the command line wins.
+occurrence of some \texttt{-i} on the command line wins.
\medskip Any \texttt{usedir} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend