# HG changeset patch
# User wenzelm
# Date 931451184 -7200
# Node ID 51c415f15007b7f97674ca143ef0c5f644688140
# Parent  f5c5b81b3f141a68b186ba061f487fda49ae920c
updated usedir;

diff -r f5c5b81b3f14 -r 51c415f15007 doc-src/System/misc.tex
--- a/doc-src/System/misc.tex	Thu Jul 08 13:55:18 1999 +0200
+++ b/doc-src/System/misc.tex	Thu Jul 08 18:26:24 1999 +0200
@@ -218,9 +218,12 @@
 Usage: usedir LOGIC NAME
 
   Options are:
-    -b           build mode (output heap image, use dir ".")
+    -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
@@ -242,23 +245,28 @@
   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.
+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 on the other hand, \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
+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 explicitely turned on or off --- the last
-occurrence of \texttt{-i} on the command line wins.
+\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