# HG changeset patch
# User wenzelm
# Date 1750069163 -7200
# Node ID d8986d88295e68061cd93f8945842416560127c0
# Parent  06372c3aa2c77ce71002c4b3922bd9d7f3fadf88
support for explicit ML platform identifier;

diff -r 06372c3aa2c7 -r d8986d88295e NEWS
--- a/NEWS	Mon Jun 16 12:18:26 2025 +0200
+++ b/NEWS	Mon Jun 16 12:19:23 2025 +0200
@@ -322,6 +322,10 @@
     isabelle build -o ML_system_64 -b HOL
     isabelle jedit -o ML_system_64
 
+* System option "ML_platform" specifies the underlying Poly/ML platform
+identifier explicitly: it takes precedence over all other options and
+settings to determine the ML_PLATFORM (see above).
+
 * System option "record_theories" tells "isabelle build" to record
 intermediate theory commands and results, at the cost of approx. 5 times
 larger ML heap images. This allows to retrieve fine-grained semantic
diff -r 06372c3aa2c7 -r d8986d88295e etc/options
--- a/etc/options	Mon Jun 16 12:18:26 2025 +0200
+++ b/etc/options	Mon Jun 16 12:19:23 2025 +0200
@@ -180,6 +180,9 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
+public option ML_platform : string = "" for build build_sync
+  -- "explicit ML platform identifier"
+
 public option ML_system_64 : bool = false for build build_sync
   -- "prefer native 64bit platform (change requires restart)"
 
diff -r 06372c3aa2c7 -r d8986d88295e src/Pure/ML/ml_settings.scala
--- a/src/Pure/ML/ml_settings.scala	Mon Jun 16 12:18:26 2025 +0200
+++ b/src/Pure/ML/ml_settings.scala	Mon Jun 16 12:19:23 2025 +0200
@@ -15,6 +15,7 @@
       override def polyml_home: Path = Path.variable("POLYML_HOME").expand_env(env)
       override def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM", env = env)
       override def ml_platform: String = {
+        proper_string(options.string("ML_platform")) orElse
         proper_string(Isabelle_System.getenv("ML_PLATFORM", env = env)) getOrElse {
           val platform_64 =
             Isabelle_Platform.make(env = env)