--- a/src/Pure/System/other_isabelle.scala Sat Jun 14 22:20:57 2025 +0200
+++ b/src/Pure/System/other_isabelle.scala Sat Jun 14 22:35:48 2025 +0200
@@ -81,17 +81,19 @@
def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
def ml_system: String = getenv_strict("ML_SYSTEM")
- def ml_platform: String = {
- val Pattern = """.*val ML_PLATFORM = "(.*)".*""".r
- val input = """val ML_PLATFORM = Option.getOpt (OS.Process.getEnv "ML_PLATFORM", "")"""
- val result = bash("bin/isabelle console -r", input = input)
- result.out match {
- case Pattern(a) if result.ok => a
- case _ =>
- error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
- if_proper(result.err, "\n" + result.err))
+ def ml_platform: String =
+ if ((isabelle_home + Path.explode("lib/Tools/console")).is_file) {
+ val Pattern = """.*val ML_PLATFORM = "(.*)".*""".r
+ val input = """val ML_PLATFORM = Option.getOpt (OS.Process.getEnv "ML_PLATFORM", "")"""
+ val result = bash("bin/isabelle console -r", input = input)
+ result.out match {
+ case Pattern(a) if result.ok => a
+ case _ =>
+ error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
+ if_proper(result.err, "\n" + result.err))
+ }
}
- }
+ else getenv("ML_PLATFORM")
def ml_identifier: String = ml_system + "_" + ml_platform
val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))