diff -r b3d458a90aeb -r a8f452f7c503 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Fri Dec 16 17:30:29 2022 +0100 +++ b/src/Pure/ML/ml_process.scala Fri Dec 16 17:51:52 2022 +0100 @@ -13,7 +13,7 @@ object ML_Process { def apply(options: Options, - base_info: Sessions.Base_Info, + 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 { - base_info.sessions_structure.selection(logic_name). + background.sessions_structure.selection(logic_name). build_requirements(List(logic_name)). map(a => File.platform_path(store.the_heap(a))) } @@ -80,7 +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(base_info.sessions_structure, base_info.base) + val resources = new Resources(background.sessions_structure, background.base) File.write(init_session, resources.init_session_yxml) // process @@ -169,10 +169,10 @@ val more_args = getopts(args) if (args.isEmpty || more_args.nonEmpty) getopts.usage() - val base_info = Sessions.base_info(options, logic, dirs = dirs).check_errors + val background = Sessions.background(options, logic, dirs = dirs).check_errors val store = Sessions.store(options) val result = - ML_Process(options, base_info, store, logic = logic, args = eval_args, modes = modes) + ML_Process(options, background, store, logic = logic, args = eval_args, modes = modes) .result( progress_stdout = Output.writeln(_, stdout = true), progress_stderr = Output.writeln(_))