# HG changeset patch
# User wenzelm
# Date 1750847344 -7200
# Node ID 88ffadf17062f4dfc3aa4d783b356369f9ef3a1f
# Parent  e891ff63e6db1a4d5ac7ff0ab771665b385700e9
clarified signature;

diff -r e891ff63e6db -r 88ffadf17062 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Wed Jun 25 12:25:02 2025 +0200
+++ b/src/Pure/Build/build.scala	Wed Jun 25 12:29:04 2025 +0200
@@ -380,7 +380,7 @@
   Notable system options: see "isabelle options -l -t build"
 
   Notable system settings:
-""" + Library.indent_lines(4, Build_Log.Settings.show(ML_Settings.system(options))) + "\n",
+""" + Library.indent_lines(4, Build_Log.Settings.show(ML_Settings(options))) + "\n",
         "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
         "B:" -> (arg => base_sessions += arg),
         "D:" -> (arg => select_dirs += Path.explode(arg)),
@@ -408,7 +408,7 @@
 
       val progress = new Console_Progress(verbose = verbose)
 
-      val ml_settings = ML_Settings.system(options)
+      val ml_settings = ML_Settings(options)
 
       progress.echo(
         "Started at " + Build_Log.print_date(progress.start) +
diff -r e891ff63e6db -r 88ffadf17062 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Wed Jun 25 12:25:02 2025 +0200
+++ b/src/Pure/Build/store.scala	Wed Jun 25 12:29:04 2025 +0200
@@ -286,7 +286,7 @@
 
   /* ML system settings */
 
-  val ml_settings: ML_Settings = ML_Settings.system(options)
+  val ml_settings: ML_Settings = ML_Settings(options)
 
   val system_output_dir: Path =
     Path.variable("ISABELLE_HEAPS_SYSTEM") + Path.basic(ml_settings.ml_identifier)
diff -r e891ff63e6db -r 88ffadf17062 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Wed Jun 25 12:25:02 2025 +0200
+++ b/src/Pure/ML/ml_process.scala	Wed Jun 25 12:29:04 2025 +0200
@@ -27,7 +27,7 @@
     cleanup: () => Unit = () => ()
   ): Bash.Process = {
     val ml_options = options.standard_ml()
-    val ml_settings = ML_Settings.system(ml_options)
+    val ml_settings = ML_Settings(ml_options)
 
     val eval_init =
       if (session_heaps.isEmpty) {
diff -r e891ff63e6db -r 88ffadf17062 src/Pure/ML/ml_settings.scala
--- a/src/Pure/ML/ml_settings.scala	Wed Jun 25 12:25:02 2025 +0200
+++ b/src/Pure/ML/ml_settings.scala	Wed Jun 25 12:29:04 2025 +0200
@@ -8,7 +8,7 @@
 
 
 object ML_Settings {
-  def system(options: Options,
+  def apply(options: Options,
     env: Isabelle_System.Settings = Isabelle_System.Settings()
   ): ML_Settings =
     new ML_Settings {
diff -r e891ff63e6db -r 88ffadf17062 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Jun 25 12:25:02 2025 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed Jun 25 12:29:04 2025 +0200
@@ -59,7 +59,7 @@
 
     val env_prefix = if_proper(stats_dir, Bash.exports("POLYSTATSDIR=" + stats_dir))
 
-    val polyml_exe = ML_Settings.system(options).polyml_exe
+    val polyml_exe = ML_Settings(options).polyml_exe
 
     Bash.process(env_prefix + File.bash_path(polyml_exe) +
         " -q --use src/Pure/ML/ml_statistics.ML --eval " +
diff -r e891ff63e6db -r 88ffadf17062 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Wed Jun 25 12:25:02 2025 +0200
+++ b/src/Pure/Tools/doc.scala	Wed Jun 25 12:29:04 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.system(Options.init() + ("ML_platform=" + arg))
+      val ml_settings = ML_Settings(Options.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.system(Options.init())
+      val ml_settings = ML_Settings(Options.init())
 
       if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
       else {
diff -r e891ff63e6db -r 88ffadf17062 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Wed Jun 25 12:25:02 2025 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Wed Jun 25 12:29:04 2025 +0200
@@ -53,7 +53,7 @@
   def session: JEdit_Session = plugin.session
   def resources: JEdit_Resources = session.resources
 
-  def ml_settings: ML_Settings = ML_Settings.system(plugin.startup_options)
+  def ml_settings: ML_Settings = ML_Settings(plugin.startup_options)
 
   object editor extends JEdit_Editor
 }