# HG changeset patch
# User wenzelm
# Date 1750847863 -7200
# Node ID e8194d5556257a802f4b64ed3f6e229e680aed1c
# Parent  88ffadf17062f4dfc3aa4d783b356369f9ef3a1f
tuned signature;

diff -r 88ffadf17062 -r e8194d555625 src/Pure/ML/ml_settings.scala
--- a/src/Pure/ML/ml_settings.scala	Wed Jun 25 12:29:04 2025 +0200
+++ b/src/Pure/ML/ml_settings.scala	Wed Jun 25 12:37:43 2025 +0200
@@ -28,6 +28,10 @@
         proper_string(Isabelle_System.getenv("ML_OPTIONS", env = env)) getOrElse
           Isabelle_System.getenv(if (ml_platform_is_64_32) "ML_OPTIONS32" else "ML_OPTIONS64")
     }
+
+  def init(ml_platform: String = ""): ML_Settings =
+    apply(Options.init(specs =
+      if (ml_platform.isEmpty) Nil else List(Options.Spec("ML_platform", Some(ml_platform)))))
 }
 
 abstract class ML_Settings {
diff -r 88ffadf17062 -r e8194d555625 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Wed Jun 25 12:29:04 2025 +0200
+++ b/src/Pure/Tools/doc.scala	Wed Jun 25 12:37:43 2025 +0200
@@ -122,7 +122,7 @@
   object Doc_Names extends Scala.Fun_String("doc_names") {
     val here = Scala_Project.here
     def apply(arg: String): String = {
-      val ml_settings = ML_Settings(Options.init() + ("ML_platform=" + arg))
+      val ml_settings = ML_Settings.init(ml_platform = arg)
       cat_lines((for (entry <- contents(ml_settings).entries(pdf = true)) yield entry.name).sorted)
     }
   }
@@ -149,7 +149,7 @@
 """)
       val docs = getopts(args)
 
-      val ml_settings = ML_Settings(Options.init())
+      val ml_settings = ML_Settings.init()
 
       if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
       else {