src/Pure/Tools/ml_console.scala
changeset 65431 4a3e6cda3b94
parent 64598 476e89d06272
--- a/src/Pure/Tools/ml_console.scala	Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/Tools/ml_console.scala	Fri Apr 07 19:35:39 2017 +0200
@@ -72,7 +72,10 @@
       val process =
         ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
           modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
-          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
+          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
+          session_base =
+            if (raw_ml_system) None
+            else Some(Sessions.session_base(options, logic, dirs)))
       val process_output = Future.thread[Unit]("process_output") {
         try {
           var result = new StringBuilder(100)