--- a/src/Pure/ML/ml_process.scala Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/ML/ml_process.scala Fri Dec 16 18:12:48 2022 +0100
@@ -13,7 +13,7 @@
object ML_Process {
def apply(options: Options,
- background: Sessions.Background,
+ session_background: Sessions.Background,
store: Sessions.Store,
logic: String = "",
raw_ml_system: Boolean = false,
@@ -31,7 +31,7 @@
val heaps: List[String] =
if (raw_ml_system) Nil
else {
- background.sessions_structure.selection(logic_name).
+ session_background.sessions_structure.selection(logic_name).
build_requirements(List(logic_name)).
map(a => File.platform_path(store.the_heap(a)))
}
@@ -80,8 +80,7 @@
val eval_init_session = if (raw_ml_system) Nil else List("Resources.init_session_env ()")
val init_session = Isabelle_System.tmp_file("init_session")
Isabelle_System.chmod("600", File.path(init_session))
- val resources = new Resources(background.sessions_structure, background.base)
- File.write(init_session, resources.init_session_yxml)
+ File.write(init_session, new Resources(session_background).init_session_yxml)
// process
val eval_process =
@@ -169,11 +168,11 @@
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
- val background = Sessions.background(options, logic, dirs = dirs).check_errors
+ val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
val store = Sessions.store(options)
val result =
- ML_Process(options, background, store, logic = logic, args = eval_args, modes = modes)
- .result(
+ ML_Process(options, session_background, store,
+ logic = logic, args = eval_args, modes = modes).result(
progress_stdout = Output.writeln(_, stdout = true),
progress_stderr = Output.writeln(_))