diff -r 8d42bf3b821d -r e1a8753eaad7 src/Pure/ML/ml_settings.scala --- a/src/Pure/ML/ml_settings.scala Sun Jun 15 13:40:03 2025 +0200 +++ b/src/Pure/ML/ml_settings.scala Sun Jun 15 15:19:03 2025 +0200 @@ -8,13 +8,11 @@ object ML_Settings { - def system(env: Isabelle_System.Settings = Isabelle_System.Settings()): System = - new System(env) - - class System(env: Isabelle_System.Settings = Isabelle_System.Settings()) extends ML_Settings { - override def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM", env = env) - override def ml_platform: String = Isabelle_System.getenv_strict("ML_PLATFORM", env = env) - } + def system(env: Isabelle_System.Settings = Isabelle_System.Settings()): ML_Settings = + new ML_Settings { + override def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM", env = env) + override def ml_platform: String = Isabelle_System.getenv_strict("ML_PLATFORM", env = env) + } } trait ML_Settings {