diff -r a8f452f7c503 -r a8d85b4a588c src/Pure/ML/ml_process.scala --- 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(_))