--- 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) +
--- 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)
--- 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) {
--- 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 {
--- 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 " +
--- 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 {
--- 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
}