tuned signature;
authorwenzelm
Sun, 26 Mar 2023 20:03:03 +0200
changeset 77719 cbfbf48b0281
parent 77718 6ad3a412ed97
child 77720 f750047e9386
tuned signature;
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build.scala
src/Tools/jEdit/src/session_build.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")
 
--- 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)
 
--- 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()