clarified Resources.init_session for low-level "isabelle process";
authorwenzelm
Mon, 16 Nov 2020 23:49:20 +0100
changeset 72867 5e616a454b23
parent 72866 8d83acc5062e
child 72868 20f70d20e6f8
child 72870 5cea0993ee4f
clarified Resources.init_session for low-level "isabelle process";
src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Mon Nov 16 23:27:43 2020 +0100
+++ b/src/Pure/ML/ml_process.scala	Mon Nov 16 23:49:20 2020 +0100
@@ -201,11 +201,11 @@
     val more_args = getopts(args)
     if (args.isEmpty || more_args.nonEmpty) getopts.usage()
 
-    val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+    val base_info = Sessions.base_info(options, logic, dirs = dirs).check
     val store = Sessions.store(options)
-
     val result =
-      ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes)
+      ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args,
+        modes = modes, session_base = Some(base_info.base))
         .result(
           progress_stdout = Output.writeln(_, stdout = true),
           progress_stderr = Output.writeln(_))