clarified signature;
authorwenzelm
Sat, 14 Jun 2025 21:19:37 +0200
changeset 82711 5bd0d6a8fd7a
parent 82710 e09e986731e9
child 82712 2f22014a3a49
clarified signature;
src/Pure/Build/build_cluster.scala
src/Pure/System/other_isabelle.scala
--- a/src/Pure/Build/build_cluster.scala	Sat Jun 14 21:07:09 2025 +0200
+++ b/src/Pure/Build/build_cluster.scala	Sat Jun 14 21:19:37 2025 +0200
@@ -208,7 +208,7 @@
     }
 
     def start(): Process_Result = {
-      val build_cluster_ml_platform = build_cluster_isabelle.getenv("ML_PLATFORM")
+      val build_cluster_ml_platform = build_cluster_isabelle.ml_platform
       if (build_cluster_ml_platform != build_context.ml_platform) {
         error("Bad ML_PLATFORM: found " + build_cluster_ml_platform +
           ", but expected " + build_context.ml_platform)
--- a/src/Pure/System/other_isabelle.scala	Sat Jun 14 21:07:09 2025 +0200
+++ b/src/Pure/System/other_isabelle.scala	Sat Jun 14 21:19:37 2025 +0200
@@ -68,12 +68,19 @@
     ssh.execute(bash_context("bin/isabelle getenv -b " + Bash.string(name)),
       settings = false).check.out
 
+  def getenv_strict(name: String): String =
+    proper_string(getenv(name)) getOrElse
+      error("Undefined Isabelle environment variable: " + quote(name) +
+        "\nISABELLE_HOME=" + isabelle_home)
+
   val settings: Isabelle_System.Settings = (name: String) => getenv(name)
 
   def expand_path(path: Path): Path = path.expand_env(settings)
   def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
 
-  def ml_identifier: String = ML_Process.ml_identifier(env = settings)
+  def ml_system: String = getenv_strict("ML_SYSTEM")
+  def ml_platform: String = getenv_strict("ML_PLATFORM")
+  def ml_identifier: String = ml_system + "_" + ml_platform
 
   val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))