--- 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
--- 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.
--- 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