--- 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)
--- 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,
--- 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")
--- 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()