diff -r 421137ff146a -r b045b40a65cc src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Wed Dec 21 13:38:41 2022 +0100 +++ b/src/Pure/ML/ml_process.scala Wed Dec 21 13:52:44 2022 +0100 @@ -12,9 +12,10 @@ object ML_Process { - def apply(options: Options, + def apply( + store: Sessions.Store, + options: Options, session_background: Sessions.Background, - store: Sessions.Store, logic: String = "", raw_ml_system: Boolean = false, use_prelude: List[String] = Nil, @@ -168,10 +169,10 @@ val more_args = getopts(args) if (args.isEmpty || more_args.nonEmpty) getopts.usage() + val store = Sessions.store(options) val session_background = Sessions.background(options, logic, dirs = dirs).check_errors - val store = Sessions.store(options) val result = - ML_Process(options, session_background, store, + ML_Process(store, options, session_background, logic = logic, args = eval_args, modes = modes).result( progress_stdout = Output.writeln(_, stdout = true), progress_stderr = Output.writeln(_))