--- 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)
--- 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(_))
--- 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
--- 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)
--- 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)
--- 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 +
--- 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")) :::