--- a/Admin/makedist Wed Nov 14 16:22:44 2007 +0100
+++ b/Admin/makedist Thu Nov 15 11:49:00 2007 +0100
@@ -194,6 +194,7 @@
} >ANNOUNCE
fi
+perl -pi -e "s/ISABELLE_IDENTIFIER=\"\"/ISABELLE_IDENTIFIER=\"$DISTNAME\"/g;" lib/scripts/getsettings
perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/library_index_header.template
perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version
perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README
--- a/NEWS Wed Nov 14 16:22:44 2007 +0100
+++ b/NEWS Thu Nov 15 11:49:00 2007 +0100
@@ -1407,9 +1407,9 @@
*** System ***
-* settings: ML_IDENTIFIER -- which is appended to user specific heap
-locations -- now includes the Isabelle version identifier as well.
-This simplifies use of multiple Isabelle installations.
+* settings: the default heap location within ISABELLE_HOME_USER now
+includes ISABELLE_IDENTIFIER. This simplifies use of multiple
+Isabelle installations.
* isabelle-process: option -S (secure mode) disables some critical
operations, notably runtime compilation and evaluation of ML source
--- a/doc-src/System/basics.tex Wed Nov 14 16:22:44 2007 +0100
+++ b/doc-src/System/basics.tex Thu Nov 15 11:49:00 2007 +0100
@@ -106,8 +106,9 @@
absolute path names of the \texttt{isabelle-process} and \texttt{isatool}
executables, respectively.
-\item \settdx{ISABELLE_OUTPUT} will have the {\ML} system and Isabelle version
- identifier (according to \texttt{ML_IDENTIFIER}) appended automatically to
+\item \settdx{ISABELLE_OUTPUT} will have the identifiers of the
+ Isabelle distribution (cf.\ \texttt{ISABELLE_IDENTIFIER}) and the
+ {\ML} system (cf.\ \texttt{ML_IDENTIFIER}) appended automatically to
its value.
\end{itemize}
@@ -141,6 +142,9 @@
that the Isabelle \texttt{bin} directory is on the current search path of
the shell.
+\item[\settdx{ISABELLE_IDENTIFIER}*] refers to the name of this
+ Isabelle distribution, e.g.\ ``\texttt{Isabelle2007}''.
+
\item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS},
\settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML}
system to be used for Isabelle. There is only a fixed set of admissable