# HG changeset patch
# User wenzelm
# Date 1749904654 -7200
# Node ID e43ef311d59574fda2d2dc4f1d220f079371e20b
# Parent  f935baefee46f2c60f76d7557c85d8bb158dd612
clarified modules;

diff -r f935baefee46 -r e43ef311d595 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sat Jun 14 14:34:11 2025 +0200
+++ b/src/Pure/Build/build.scala	Sat Jun 14 14:37:34 2025 +0200
@@ -409,7 +409,7 @@
 
       progress.echo(
         "Started at " + Build_Log.print_date(progress.start) +
-          " (" + Isabelle_System.ml_identifier() + " on " + hostname(options) +")",
+          " (" + ML_Process.ml_identifier() + " on " + hostname(options) +")",
         verbose = true)
       progress.echo(Build_Log.Settings.show() + "\n", verbose = true)
 
diff -r f935baefee46 -r e43ef311d595 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Jun 14 14:34:11 2025 +0200
+++ b/src/Pure/ML/ml_process.scala	Sat Jun 14 14:37:34 2025 +0200
@@ -11,6 +11,14 @@
 
 
 object ML_Process {
+  /* settings */
+
+  def ml_identifier(env: Isabelle_System.Settings = Isabelle_System.Settings()): String =
+    Isabelle_System.getenv("ML_IDENTIFIER", env = env)
+
+
+  /* heaps */
+
   def make_shasum(ancestors: List[SHA1.Shasum]): SHA1.Shasum =
     if (ancestors.isEmpty) SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
     else SHA1.flat_shasum(ancestors)
@@ -27,6 +35,9 @@
       map(name => store.get_session(name).the_heap)
   }
 
+
+  /* process */
+
   def apply(
     options: Options,
     session_background: Sessions.Background,
diff -r f935baefee46 -r e43ef311d595 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Jun 14 14:34:11 2025 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jun 14 14:37:34 2025 +0200
@@ -51,8 +51,6 @@
     proper_string(getenv(name, env)) getOrElse
       error("Undefined Isabelle environment variable: " + quote(name))
 
-  def ml_identifier(): String = getenv("ML_IDENTIFIER")
-
   def hostname(default: String = ""): String =
     proper_string(default) getOrElse getenv_strict("ISABELLE_HOSTNAME")
 
diff -r f935baefee46 -r e43ef311d595 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Jun 14 14:34:11 2025 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sat Jun 14 14:37:34 2025 +0200
@@ -146,7 +146,7 @@
 
     /* main */
 
-    setTitle("Isabelle build (" + Isabelle_System.ml_identifier() + " / " +
+    setTitle("Isabelle build (" + ML_Process.ml_identifier() + " / " +
       "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
 
     pack()