--- a/src/Pure/ML/ml_console.scala Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/ML/ml_console.scala Fri Mar 27 12:46:56 2020 +0100
@@ -51,6 +51,7 @@
val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+ val store = Sessions.store(options)
// build logic
if (!no_build && !raw_ml_system) {
@@ -64,10 +65,10 @@
// process loop
val process =
- ML_Process(options, sessions_structure, logic = logic, args = List("-i"), redirect = true,
+ ML_Process(options, sessions_structure, store,
+ logic = logic, args = List("-i"), redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system,
- store = Some(Sessions.store(options)),
session_base =
if (raw_ml_system) None
else Some(Sessions.base_info(