# HG changeset patch
# User wenzelm
# Date 1749913818 -7200
# Node ID 1008b8e7c78d1131d97d9364fb6de992015ab6ef
# Parent  e43ef311d59574fda2d2dc4f1d220f079371e20b
discontinued ML_IDENTIFIER settings variable;

diff -r e43ef311d595 -r 1008b8e7c78d NEWS
--- a/NEWS	Sat Jun 14 14:37:34 2025 +0200
+++ b/NEWS	Sat Jun 14 17:10:18 2025 +0200
@@ -302,6 +302,11 @@
 
 *** System ***
 
+* The traditional ML system settings have been reconsidered: this
+affects ML_IDENTIFIER (discontinued). Potential INCOMPATIBILITY for old
+shell scripts --- better use Isabelle/Scala operations from module
+ML_Process or Store.
+
 * System option "record_theories" tells "isabelle build" to record
 intermediate theory commands and results, at the cost of approx. 5 times
 larger ML heap images. This allows to retrieve fine-grained semantic
diff -r e43ef311d595 -r 1008b8e7c78d lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sat Jun 14 14:37:34 2025 +0200
+++ b/lib/scripts/getsettings	Sat Jun 14 17:10:18 2025 +0200
@@ -103,13 +103,6 @@
     ;;
 esac
 
-#ML system identifier
-if [ -z "$ML_PLATFORM" ]; then
-  ML_IDENTIFIER="$ML_SYSTEM"
-else
-  ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
-fi
-
 #enforce ISABELLE_OCAMLFIND
 if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]; then
   ISABELLE_OCAMLFIND="$ISABELLE_HOME/lib/scripts/ocamlfind"
diff -r e43ef311d595 -r 1008b8e7c78d src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Doc/System/Environment.thy	Sat Jun 14 17:10:18 2025 +0200
@@ -138,18 +138,13 @@
   Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2025\<close>''.
 
   \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
-  ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
-  specify the underlying ML system to be used for Isabelle. There is only a
-  fixed set of admissable @{setting ML_SYSTEM} names (see the
-  \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution).
+  ML_OPTIONS}, @{setting_def ML_PLATFORM}] specify the underlying ML system of
+  Isabelle.
 
   The actual compiler binary will be run from the directory @{setting
   ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
   The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
-  images, which is useful for cross-platform installations. The value of
-  @{setting ML_IDENTIFIER} is automatically obtained by composing the values
-  of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
-  values.
+  images, which is useful for cross-platform installations.
 
   \<^descr>[@{setting_def ISABELLE_JDK_HOME}] points to a full JDK (Java Development
   Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. Note that
diff -r e43ef311d595 -r 1008b8e7c78d src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Jun 14 17:10:18 2025 +0200
@@ -204,9 +204,7 @@
       File.write(other_isabelle.etc_preferences,
         cat_lines("build_log_verbose = true" :: more_preferences))
 
-      val isabelle_output =
-        other_isabelle.expand_path(
-          Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER"))
+      val isabelle_output = other_isabelle.user_output_dir
       val isabelle_output_log = isabelle_output + Path.explode("log")
       val isabelle_base_log = isabelle_output + Path.explode("../base_log")
 
diff -r e43ef311d595 -r 1008b8e7c78d src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/Build/build.scala	Sat Jun 14 17:10:18 2025 +0200
@@ -31,7 +31,6 @@
     engine: Engine = Engine.Default,
     afp_root: Option[Path] = None,
     build_hosts: List[Build_Cluster.Host] = Nil,
-    ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
     hostname: String = Isabelle_System.hostname(),
     numa_shuffling: Boolean = false,
     numa_nodes: List[Int] = Nil,
@@ -47,6 +46,8 @@
   ) {
     def build_options: Options = store.options
 
+    def ml_platform: String = store.ml_platform
+
     def sessions_structure: isabelle.Sessions.Structure = deps.sessions_structure
 
     def worker: Boolean = jobs > 0
diff -r e43ef311d595 -r 1008b8e7c78d src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/Build/store.scala	Sat Jun 14 17:10:18 2025 +0200
@@ -14,8 +14,9 @@
   def apply(
     options: Options,
     build_cluster: Boolean = false,
-    cache: Term.Cache = Term.Cache.make()
-  ): Store = new Store(options, build_cluster, cache)
+    cache: Term.Cache = Term.Cache.make(),
+    other_ml_platform: Option[String] = None
+  ): Store = new Store(options, build_cluster, cache, other_ml_platform)
 
 
   /* file names */
@@ -277,17 +278,25 @@
 class Store private(
     val options: Options,
     val build_cluster: Boolean,
-    val cache: Term.Cache
+    val cache: Term.Cache,
+    other_ml_platform: Option[String]
   ) {
   store =>
 
   override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
 
+  /* ML system */
+
+  def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM")
+  def ml_platform: String = other_ml_platform getOrElse Isabelle_System.getenv_strict("ML_PLATFORM")
+  def ml_identifier: String = ml_system + "_" + ml_platform
+
+
   /* directories */
 
-  val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
-  val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
+  val system_output_dir: Path = Path.variable("ISABELLE_HEAPS_SYSTEM") + Path.basic(ml_identifier)
+  val user_output_dir: Path = Path.variable("ISABELLE_HEAPS") + Path.basic(ml_identifier)
 
   def system_heaps: Boolean = options.bool("system_heaps")
 
diff -r e43ef311d595 -r 1008b8e7c78d src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/ML/ml_process.scala	Sat Jun 14 17:10:18 2025 +0200
@@ -14,7 +14,8 @@
   /* settings */
 
   def ml_identifier(env: Isabelle_System.Settings = Isabelle_System.Settings()): String =
-    Isabelle_System.getenv("ML_IDENTIFIER", env = env)
+    Isabelle_System.getenv_strict("ML_SYSTEM", env = env) + "_" +
+    Isabelle_System.getenv_strict("ML_PLATFORM", env = env)
 
 
   /* heaps */
diff -r e43ef311d595 -r 1008b8e7c78d src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/System/other_isabelle.scala	Sat Jun 14 17:10:18 2025 +0200
@@ -73,8 +73,12 @@
   def expand_path(path: Path): Path = path.expand_env(settings)
   def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
 
+  def ml_identifier: String = ML_Process.ml_identifier(env = settings)
+
   val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))
 
+  def user_output_dir: Path = isabelle_home_user + Path.basic("heaps") + Path.basic(ml_identifier)
+
   def host_db: Path = isabelle_home_user + Path.explode("host.db")
 
   def etc: Path = isabelle_home_user + Path.explode("etc")