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(_))