# HG changeset patch
# User wenzelm
# Date 1671627164 -3600
# Node ID b045b40a65cc13a050f28947fec498ce54eed8c8
# Parent  421137ff146a6f376ba45e565ba618c2b726caff
clarified signature;

diff -r 421137ff146a -r b045b40a65cc src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Wed Dec 21 13:38:41 2022 +0100
+++ b/src/Pure/ML/ml_console.scala	Wed Dec 21 13:52:44 2022 +0100
@@ -60,7 +60,7 @@
         if (rc != Process_Result.RC.ok) sys.exit(rc)
       }
 
-      val background =
+      val session_background =
         if (raw_ml_system) {
           Sessions.Background(
             base = Sessions.Base.bootstrap,
@@ -73,7 +73,7 @@
 
       // process loop
       val process =
-        ML_Process(options, background, store,
+        ML_Process(store, options, session_background,
           logic = logic, args = List("-i"), redirect = true,
           modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
           raw_ml_system = raw_ml_system)
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(_))
diff -r 421137ff146a -r b045b40a65cc src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Dec 21 13:38:41 2022 +0100
+++ b/src/Pure/PIDE/headless.scala	Wed Dec 21 13:52:44 2022 +0100
@@ -622,7 +622,7 @@
       val session = new Session(session_name, options, resources)
 
       progress.echo("Starting session " + session_name + " ...")
-      Isabelle_Process.start(session, options, session_background, store,
+      Isabelle_Process.start(store, options, session, session_background,
         logic = session_name, modes = print_mode).await_startup()
 
       session
diff -r 421137ff146a -r b045b40a65cc src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Wed Dec 21 13:38:41 2022 +0100
+++ b/src/Pure/System/isabelle_process.scala	Wed Dec 21 13:52:44 2022 +0100
@@ -13,10 +13,10 @@
 
 object Isabelle_Process {
   def start(
-    session: Session,
+    store: Sessions.Store,
     options: Options,
+    session: Session,
     session_background: Sessions.Background,
-    store: Sessions.Store,
     logic: String = "",
     raw_ml_system: Boolean = false,
     use_prelude: List[String] = Nil,
@@ -28,10 +28,11 @@
     val channel = System_Channel()
     val process =
       try {
-        val channel_options =
-          options.string.update("system_channel_address", channel.address).
+        val ml_options =
+          options.
+            string.update("system_channel_address", channel.address).
             string.update("system_channel_password", channel.password)
-        ML_Process(channel_options, session_background, store,
+        ML_Process(store, ml_options, session_background,
           logic = logic, raw_ml_system = raw_ml_system,
           use_prelude = use_prelude, eval_main = eval_main,
           modes = modes, cwd = cwd, env = env)
diff -r 421137ff146a -r b045b40a65cc src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Dec 21 13:38:41 2022 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Dec 21 13:52:44 2022 +0100
@@ -447,7 +447,7 @@
       val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
       val process =
-        Isabelle_Process.start(session, options, session_background, store,
+        Isabelle_Process.start(store, options, session, session_background,
           logic = parent, raw_ml_system = is_pure,
           use_prelude = use_prelude, eval_main = eval_main,
           cwd = info.dir.file, env = env)
diff -r 421137ff146a -r b045b40a65cc src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Wed Dec 21 13:38:41 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Dec 21 13:52:44 2022 +0100
@@ -307,7 +307,7 @@
       dynamic_output.init()
 
       try {
-        Isabelle_Process.start(session, options, session_background, store,
+        Isabelle_Process.start(store, options, session, session_background,
           modes = modes, logic = session_background.session_name).await_startup()
         reply_ok(
           "Welcome to Isabelle/" + session_background.session_name +
diff -r 421137ff146a -r b045b40a65cc src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Dec 21 13:38:41 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Dec 21 13:52:44 2022 +0100
@@ -151,7 +151,7 @@
 
     session.phase_changed += PIDE.plugin.session_phase_changed
 
-    Isabelle_Process.start(session, store.options, session_background, store,
+    Isabelle_Process.start(store, store.options, session, session_background,
       logic = session_background.session_name,
       modes =
         (space_explode(',', store.options.string("jedit_print_mode")) :::