--- 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 {
--- 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 {