# HG changeset patch
# User wenzelm
# Date 1749993543 -7200
# Node ID e1a8753eaad71284826aa8828d9e0681a7311082
# Parent  8d42bf3b821de12b04871aceba0967a36aa59c49
clarified signature: more modular, avoid adhoc mixins;

diff -r 8d42bf3b821d -r e1a8753eaad7 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sun Jun 15 13:40:03 2025 +0200
+++ b/src/Pure/Build/build.scala	Sun Jun 15 15:19:03 2025 +0200
@@ -46,7 +46,7 @@
   ) {
     def build_options: Options = store.options
 
-    def ml_platform: String = store.ml_platform
+    def ml_platform: String = store.ml_settings.ml_platform
 
     def sessions_structure: isabelle.Sessions.Structure = deps.sessions_structure
 
diff -r 8d42bf3b821d -r e1a8753eaad7 src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Sun Jun 15 13:40:03 2025 +0200
+++ b/src/Pure/Build/build_cluster.scala	Sun Jun 15 15:19:03 2025 +0200
@@ -208,7 +208,7 @@
     }
 
     def start(): Process_Result = {
-      val build_cluster_ml_platform = build_cluster_isabelle.ml_platform
+      val build_cluster_ml_platform = build_cluster_isabelle.ml_settings.ml_platform
       if (build_cluster_ml_platform != build_context.ml_platform) {
         error("Bad ML_PLATFORM: found " + build_cluster_ml_platform +
           ", but expected " + build_context.ml_platform)
diff -r 8d42bf3b821d -r e1a8753eaad7 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Sun Jun 15 13:40:03 2025 +0200
+++ b/src/Pure/Build/store.scala	Sun Jun 15 15:19:03 2025 +0200
@@ -278,16 +278,24 @@
     val options: Options,
     val build_cluster: Boolean,
     val cache: Term.Cache
-  ) extends ML_Settings.System() {
+  ) {
   store =>
 
   override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
 
-  /* directories */
+  /* ML system settings */
+
+  val ml_settings: ML_Settings = ML_Settings.system()
 
-  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)
+  val system_output_dir: Path =
+    Path.variable("ISABELLE_HEAPS_SYSTEM") + Path.basic(ml_settings.ml_identifier)
+
+  val user_output_dir: Path =
+    Path.variable("ISABELLE_HEAPS") + Path.basic(ml_settings.ml_identifier)
+
+
+  /* directories */
 
   def system_heaps: Boolean = options.bool("system_heaps")
 
diff -r 8d42bf3b821d -r e1a8753eaad7 src/Pure/ML/ml_settings.scala
--- a/src/Pure/ML/ml_settings.scala	Sun Jun 15 13:40:03 2025 +0200
+++ b/src/Pure/ML/ml_settings.scala	Sun Jun 15 15:19:03 2025 +0200
@@ -8,13 +8,11 @@
 
 
 object ML_Settings {
-  def system(env: Isabelle_System.Settings = Isabelle_System.Settings()): System =
-    new System(env)
-
-  class System(env: Isabelle_System.Settings = Isabelle_System.Settings()) extends ML_Settings {
-    override def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM", env = env)
-    override def ml_platform: String = Isabelle_System.getenv_strict("ML_PLATFORM", env = env)
-  }
+  def system(env: Isabelle_System.Settings = Isabelle_System.Settings()): ML_Settings =
+    new ML_Settings {
+      override def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM", env = env)
+      override def ml_platform: String = Isabelle_System.getenv_strict("ML_PLATFORM", env = env)
+    }
 }
 
 trait ML_Settings {
diff -r 8d42bf3b821d -r e1a8753eaad7 src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Sun Jun 15 13:40:03 2025 +0200
+++ b/src/Pure/System/other_isabelle.scala	Sun Jun 15 15:19:03 2025 +0200
@@ -35,7 +35,7 @@
   isabelle_home_url: String,
   val ssh: SSH.System,
   val progress: Progress
-) extends ML_Settings {
+) {
   other_isabelle =>
 
   override def toString: String = isabelle_home_url
@@ -82,8 +82,6 @@
 
   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")
@@ -91,23 +89,29 @@
   def etc_preferences: Path = etc + Path.explode("preferences")
 
 
-  /* ML system */
+  /* ML system settings */
 
-  override def ml_system: String = getenv_strict("ML_SYSTEM")
+  val ml_settings: ML_Settings =
+    new ML_Settings {
+      override def ml_system: String = getenv_strict("ML_SYSTEM")
 
-  override def ml_platform: String =
-    if ((isabelle_home + Path.explode("lib/Tools/console")).is_file) {
-      val Pattern = """.*val ML_PLATFORM = "(.*)".*""".r
-      val input = """val ML_PLATFORM = Option.getOpt (OS.Process.getEnv "ML_PLATFORM", "")"""
-      val result = bash("bin/isabelle console -r", input = input)
-      result.out match {
-        case Pattern(a) if result.ok => a
-        case _ =>
-          error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
-            if_proper(result.err, "\n" + result.err))
-      }
+      override def ml_platform: String =
+        if ((isabelle_home + Path.explode("lib/Tools/console")).is_file) {
+          val Pattern = """.*val ML_PLATFORM = "(.*)".*""".r
+          val input = """val ML_PLATFORM = Option.getOpt (OS.Process.getEnv "ML_PLATFORM", "")"""
+          val result = bash("bin/isabelle console -r", input = input)
+          result.out match {
+            case Pattern(a) if result.ok => a
+            case _ =>
+              error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
+                if_proper(result.err, "\n" + result.err))
+          }
+        }
+        else getenv("ML_PLATFORM")
     }
-    else getenv("ML_PLATFORM")
+
+  def user_output_dir: Path =
+    isabelle_home_user + Path.basic("heaps") + Path.basic(ml_settings.ml_identifier)
 
 
   /* components */