# HG changeset patch
# User wenzelm
# Date 1749986017 -7200
# Node ID 6e33d46b14007bb79ceaacce43131c086c9ff669
# Parent  a71d0beff950fef0db8bfd2129d95db97f4cda3c
clarified signature: more explicit types;

diff -r a71d0beff950 -r 6e33d46b1400 etc/build.props
--- a/etc/build.props	Sat Jun 14 22:35:48 2025 +0200
+++ b/etc/build.props	Sun Jun 15 13:13:37 2025 +0200
@@ -158,6 +158,7 @@
   src/Pure/ML/ml_lex.scala \
   src/Pure/ML/ml_process.scala \
   src/Pure/ML/ml_profiling.scala \
+  src/Pure/ML/ml_settings.scala \
   src/Pure/ML/ml_statistics.scala \
   src/Pure/ML/ml_syntax.scala \
   src/Pure/PIDE/byte_message.scala \
diff -r a71d0beff950 -r 6e33d46b1400 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sat Jun 14 22:35:48 2025 +0200
+++ b/src/Pure/Build/build.scala	Sun Jun 15 13:13:37 2025 +0200
@@ -410,7 +410,7 @@
 
       progress.echo(
         "Started at " + Build_Log.print_date(progress.start) +
-          " (" + ML_Process.ml_identifier() + " on " + hostname(options) +")",
+          " (" + ML_Settings.system().ml_identifier + " on " + hostname(options) +")",
         verbose = true)
       progress.echo(Build_Log.Settings.show() + "\n", verbose = true)
 
diff -r a71d0beff950 -r 6e33d46b1400 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Sat Jun 14 22:35:48 2025 +0200
+++ b/src/Pure/Build/store.scala	Sun Jun 15 13:13:37 2025 +0200
@@ -278,19 +278,12 @@
     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 + ")"
 
 
-  /* ML system */
-
-  def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM")
-  def ml_platform: String = Isabelle_System.getenv_strict("ML_PLATFORM")
-  def ml_identifier: String = ml_system + "_" + ml_platform
-
-
   /* directories */
 
   val system_output_dir: Path = Path.variable("ISABELLE_HEAPS_SYSTEM") + Path.basic(ml_identifier)
diff -r a71d0beff950 -r 6e33d46b1400 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Jun 14 22:35:48 2025 +0200
+++ b/src/Pure/ML/ml_process.scala	Sun Jun 15 13:13:37 2025 +0200
@@ -11,13 +11,6 @@
 
 
 object ML_Process {
-  /* settings */
-
-  def ml_identifier(env: Isabelle_System.Settings = Isabelle_System.Settings()): String =
-    Isabelle_System.getenv_strict("ML_SYSTEM", env = env) + "_" +
-    Isabelle_System.getenv_strict("ML_PLATFORM", env = env)
-
-
   /* heaps */
 
   def make_shasum(ancestors: List[SHA1.Shasum]): SHA1.Shasum =
diff -r a71d0beff950 -r 6e33d46b1400 src/Pure/ML/ml_settings.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_settings.scala	Sun Jun 15 13:13:37 2025 +0200
@@ -0,0 +1,24 @@
+/*  Title:      Pure/ML/ml_settings.scala
+    Author:     Makarius
+
+ML system settings.
+*/
+
+package isabelle
+
+
+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)
+  }
+}
+
+trait ML_Settings {
+  def ml_system: String
+  def ml_platform: String
+  def ml_identifier: String = ml_system + "_" + ml_platform
+}
diff -r a71d0beff950 -r 6e33d46b1400 src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Sat Jun 14 22:35:48 2025 +0200
+++ b/src/Pure/System/other_isabelle.scala	Sun Jun 15 13:13:37 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
@@ -80,8 +80,22 @@
   def expand_path(path: Path): Path = path.expand_env(settings)
   def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
 
-  def ml_system: String = getenv_strict("ML_SYSTEM")
-  def ml_platform: String =
+  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")
+  def etc_settings: Path = etc + Path.explode("settings")
+  def etc_preferences: Path = etc + Path.explode("preferences")
+
+
+  /* ML system */
+
+  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", "")"""
@@ -94,17 +108,6 @@
       }
     }
     else getenv("ML_PLATFORM")
-  def ml_identifier: String = ml_system + "_" + ml_platform
-
-  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")
-  def etc_settings: Path = etc + Path.explode("settings")
-  def etc_preferences: Path = etc + Path.explode("preferences")
 
 
   /* components */
diff -r a71d0beff950 -r 6e33d46b1400 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Jun 14 22:35:48 2025 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sun Jun 15 13:13:37 2025 +0200
@@ -146,7 +146,7 @@
 
     /* main */
 
-    setTitle("Isabelle build (" + ML_Process.ml_identifier() + " / " +
+    setTitle("Isabelle build (" + ML_Settings.system().ml_identifier + " / " +
       "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
 
     pack()