# HG changeset patch
# User wenzelm
# Date 923992470 -7200
# Node ID d1bbea22217b66d3ad353a6b4bca9fd49f6499c8
# Parent  b2f2770ef8d9e8f5c690acdde4b61d57c91a64ef
tuned;

diff -r b2f2770ef8d9 -r d1bbea22217b doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Mon Apr 12 16:20:04 1999 +0200
+++ b/doc-src/System/basics.tex	Tue Apr 13 10:34:30 1999 +0200
@@ -113,10 +113,10 @@
 \item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to
   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 (as specified by \texttt{ML_SYSTEM})
-  automatically appended to their values.
+  
+\item \settdx{ISABELLE_PATH} and \settdx{ISABELLE_OUTPUT} will have the {\ML}
+  system identifier (according to \texttt{ML_IDENTIFIER} automatically
+  appended to their values.
 \end{itemize}
 
 \medskip The Isabelle settings scheme is basically quite simple, but
@@ -153,18 +153,19 @@
   search path of the shell.
   
 \item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS},
-  \settdx{ML_PLATFORM}] specify the underlying {\ML} system to be used for
-  Isabelle.  The choice of \texttt{ML_SYSTEM} identifiers is quite fixed, see
-  the global \texttt{etc/settings} file for some examples. The actual compiler
-  binary will be run from directory \texttt{ML_HOME}, with \texttt{ML_OPTIONS}
-  as first arguments on the command line.  The optional \texttt{ML_PLATFORM}
-  specifies the binary format of ML heap images, which is useful for
-  cross-platform installations.
-
-\item[\settdx{ISABELLE_PATH}*] is a list of directories (separated by
-  colons) where Isabelle logic images may reside. Note that the
-  \texttt{ML_SYSTEM} identifier is appended to each component
-  automatically.
+  \settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML}
+  system to be used for Isabelle.  The choice of \texttt{ML_SYSTEM}
+  identifiers is quite fixed, see the global \texttt{etc/settings} file for
+  some examples. The actual compiler binary will be run from directory
+  \texttt{ML_HOME}, with \texttt{ML_OPTIONS} as first arguments on the command
+  line.  The optional \texttt{ML_PLATFORM} specifies the binary format of ML
+  heap images, which is useful for cross-platform installations.  The value of
+  \texttt{ML_IDENTIFIER} is (automatically) obtained by composing
+  \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}.
+  
+\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_OUTPUT}*] is a directory where output heap
   files should be stored by default. The \texttt{ML_SYSTEM} identifier
diff -r b2f2770ef8d9 -r d1bbea22217b doc-src/System/misc.tex
--- a/doc-src/System/misc.tex	Mon Apr 12 16:20:04 1999 +0200
+++ b/doc-src/System/misc.tex	Tue Apr 13 10:34:30 1999 +0200
@@ -56,9 +56,9 @@
 
   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}. Thus switching to another
+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.
 
 
diff -r b2f2770ef8d9 -r d1bbea22217b doc-src/System/system.ind
--- a/doc-src/System/system.ind	Mon Apr 12 16:20:04 1999 +0200
+++ b/doc-src/System/system.ind	Tue Apr 13 10:34:30 1999 +0200
@@ -40,7 +40,7 @@
   \item {\tt ISABELLE_INTERFACE} setting, 4, 7
   \item {\tt ISABELLE_LOGIC} setting, 4
   \item {\tt ISABELLE_OUTPUT} setting, 3, 4
-  \item {\tt ISABELLE_PATH} setting, 3
+  \item {\tt ISABELLE_PATH} setting, 3, 4
   \item {\tt ISABELLE_TMP_PREFIX} setting, 4
   \item {\tt ISABELLE_TOOLS} setting, 4
   \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 12, 17
@@ -57,6 +57,7 @@
   \item {\tt make} tool, 11
   \item {\tt makeall} tool, 12
   \item {\tt ML_HOME} setting, 3
+  \item {\tt ML_IDENTIFIER} setting, 3
   \item {\tt ML_OPTIONS} setting, 3
   \item {\tt ML_PLATFORM} setting, 3
   \item {\tt ML_SYSTEM} setting, 3