# HG changeset patch
# User wenzelm
# Date 1679853783 -7200
# Node ID cbfbf48b0281a28f9285719ed996562b60e7bf20
# Parent  6ad3a412ed976931d6f018530b7e0ff7ac3c9cc7
tuned signature;

diff -r 6ad3a412ed97 -r cbfbf48b0281 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Mar 26 19:51:35 2023 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Mar 26 20:03:03 2023 +0200
@@ -47,6 +47,8 @@
     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 6ad3a412ed97 -r cbfbf48b0281 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Mar 26 19:51:35 2023 +0200
+++ b/src/Pure/Tools/build.scala	Sun Mar 26 20:03:03 2023 +0200
@@ -331,7 +331,7 @@
 
       progress.echo(
         "Started at " + Build_Log.print_date(start_date) +
-          " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + hostname(options) +")",
+          " (" + Isabelle_System.ml_identifier() + " on " + hostname(options) +")",
         verbose = true)
       progress.echo(Build_Log.Settings.show() + "\n", verbose = true)
 
diff -r 6ad3a412ed97 -r cbfbf48b0281 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sun Mar 26 19:51:35 2023 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sun Mar 26 20:03:03 2023 +0200
@@ -146,8 +146,7 @@
 
     /* main */
 
-    setTitle("Isabelle build (" +
-      Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
+    setTitle("Isabelle build (" + Isabelle_System.ml_identifier() + " / " +
       "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
 
     pack()