# HG changeset patch
# User wenzelm
# Date 967824065 -7200
# Node ID 978c635c77f6fa28d199b556a710eb6596237f3a
# Parent  7e5e6c47c0b5534207951a1dbe64d5b56c361d97
ISABELLE_PATH: ML_IDENTIFIER no longer added;
tuned;

diff -r 7e5e6c47c0b5 -r 978c635c77f6 doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Fri Sep 01 17:54:58 2000 +0200
+++ b/doc-src/System/basics.tex	Fri Sep 01 18:01:05 2000 +0200
@@ -106,9 +106,8 @@
   the absolute path names of the \texttt{isabelle} and
   \texttt{isatool} executables, respectively.
   
-\item \settdx{ISABELLE_PATH} and \settdx{ISABELLE_OUTPUT} will have the {\ML}
-  system identifier (according to \texttt{ML_IDENTIFIER}) automatically
-  appended to their values.
+\item \settdx{ISABELLE_OUTPUT} will has the {\ML} system identifier (according
+  to \texttt{ML_IDENTIFIER}) automatically appended to its value.
 \end{itemize}
 
 \medskip The Isabelle settings scheme is basically simple, but non-trivial.
@@ -153,9 +152,9 @@
   \texttt{ML_IDENTIFIER} is automatically obtained by composing the
   \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM} values.
   
-\item[\settdx{ISABELLE_PATH}*] is a list of directories (separated by colons)
-  where Isabelle logic images may reside. Note that the value of
-  \texttt{ML_IDENTIFIER} is appended to each component automatically.
+\item[\settdx{ISABELLE_PATH}] is a list of directories (separated by colons)
+  where Isabelle logic images may reside.  When looking up heaps files, the
+  value of \texttt{ML_IDENTIFIER} is appended to each component internally.
   
 \item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap files should
   be stored by default. The \texttt{ML_SYSTEM} identifier is appended here,
@@ -230,10 +229,11 @@
 \end{ttbox}
 Input files without path specifications are looked up in the
 \texttt{ISABELLE_PATH} setting, which may consist of multiple components
-separated by colons --- these are tried in the given order.  Likewise, base
-names are relative to the directory specified by \texttt{ISABELLE_OUTPUT}.  In
-any case, actual file locations may also be given by including at least one
-slash (\texttt{/}) in the name (hint: use \texttt{./} to refer to the current
+separated by colons --- these are tried in the given order with the value of
+\texttt{ML_IDENTIFIER} appended internally.  In a similar way, base names are
+relative to the directory specified by \texttt{ISABELLE_OUTPUT}.  In any case,
+actual file locations may also be given by including at least one slash
+(\texttt{/}) in the name (hint: use \texttt{./} to refer to the current
 directory).
 
 
diff -r 7e5e6c47c0b5 -r 978c635c77f6 doc-src/System/misc.tex
--- a/doc-src/System/misc.tex	Fri Sep 01 17:54:58 2000 +0200
+++ b/doc-src/System/misc.tex	Fri Sep 01 18:01:05 2000 +0200
@@ -55,9 +55,10 @@
   Collect heap file names from ISABELLE_PATH.
 \end{ttbox}
 The base names of all files found on the path are printed --- sorted and with
-duplicates removed. Also note that \texttt{ISABELLE_PATH} implicitly depends
-upon \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}. Thus switching to another
-{\ML} compiler may change the set of logic images available.
+duplicates removed. Also note that lookup in \texttt{ISABELLE_PATH} includes
+the current values of \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}. Thus
+switching to another {\ML} compiler may change the set of logic images
+available.
 
 
 \section{Inspecting the settings environment -- \texttt{isatool getenv}}
@@ -85,29 +86,27 @@
 
 \subsection*{Examples}
 
-Get the {\ML} system identifier and the location where the compiler binaries
-are supposed to reside as follows:
+Get the {\ML} system name and the location where the compiler binaries are
+supposed to reside as follows:
 \begin{ttbox}
 isatool getenv ML_SYSTEM ML_HOME
-{\out ML_SYSTEM=smlnj-110}
-{\out ML_HOME=/usr/local/smlnj-110/bin}
+{\out ML_SYSTEM=polyml}
+{\out ML_HOME=/usr/share/polyml/x86-linux}
 \end{ttbox}
 
-The next one peeks at the search path that \texttt{isabelle} uses to locate
-logic images:
+The next one peeks at the output directory for \texttt{isabelle} logic images:
 \begin{ttbox}
-isatool getenv -b ISABELLE_PATH
-{\out /home/me/isabelle/heaps/smlnj-110:/usr/local/isabelle/heaps/smlnj-110}
+isatool getenv -b ISABELLE_OUTPUT
+{\out /home/me/isabelle/heaps/polyml_x86-linux}
 \end{ttbox}
 Here we have used the \texttt{-b} option to suppress the
-\texttt{ISABELLE_PATH=} prefix.  The value above is what became of the
+\texttt{ISABELLE_OUTPUT=} prefix.  The value above is what became of the
 following assignment in the default settings file:
 \begin{ttbox}
-ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps
+ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
 \end{ttbox}
-Note how the \texttt{ML_SYSTEM} value got appended automatically to each path
-component. This is a special feature of \texttt{ISABELLE_PATH} (and also of
-\texttt{ISABELLE_OUTPUT}).
+Note how the \texttt{ML_IDENTIFIER} value got appended automatically to each
+path component. This is a special feature of \texttt{ISABELLE_OUTPUT}.
 
 
 \section{Installing standalone Isabelle executables -- \texttt{isatool install}}