# HG changeset patch # User wenzelm # Date 1749933348 -7200 # Node ID a71d0beff950fef0db8bfd2129d95db97f4cda3c # Parent 08dec4389293acb59f859effd5c68d66bdfe6861 proper support for old versions before 0e41f26a0250; diff -r 08dec4389293 -r a71d0beff950 src/Pure/System/other_isabelle.scala --- 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"))