diff -r a3177042863d -r b3d458a90aeb src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala Fri Dec 16 17:02:10 2022 +0100 +++ b/src/Pure/ML/ml_console.scala Fri Dec 16 17:30:29 2022 +0100 @@ -48,7 +48,6 @@ if (more_args.nonEmpty) getopts.usage() - val sessions_structure = Sessions.load_structure(options, dirs = dirs) val store = Sessions.store(options) // build logic @@ -61,16 +60,23 @@ if (rc != Process_Result.RC.ok) sys.exit(rc) } + val base_info = + if (raw_ml_system) { + Sessions.Base_Info( + base = Sessions.Base.bootstrap, + sessions_structure = Sessions.load_structure(options, dirs = dirs)) + } + else { + Sessions.base_info( + options, logic, dirs = dirs, include_sessions = include_sessions).check_errors + } + // process loop val process = - ML_Process(options, sessions_structure, store, + ML_Process(options, base_info, store, logic = logic, args = List("-i"), redirect = true, modes = if (raw_ml_system) Nil else modes ::: List("ASCII"), - raw_ml_system = raw_ml_system, - session_base = - if (raw_ml_system) None - else Some(Sessions.base_info( - options, logic, dirs = dirs, include_sessions = include_sessions).check_errors.base)) + raw_ml_system = raw_ml_system) POSIX_Interrupt.handler { process.interrupt() } { new TTY_Loop(process.stdin, process.stdout).join()