src/Pure/ML/ml_process.scala

--- a/src/Pure/ML/ml_process.scala	Thu May 17 14:50:48 2018 +0200
+++ b/src/Pure/ML/ml_process.scala	Thu May 17 15:38:36 2018 +0200
@@ -23,7 +23,7 @@
     redirect: Boolean = false,
     cleanup: () => Unit = () => (),
     channel: Option[System_Channel] = None,
-    sessions: Option[Sessions.Structure] = None,
+    sessions_structure: Option[Sessions.Structure] = None,
     session_base: Option[Sessions.Base] = None,
     store: Sessions.Store = Sessions.store()): Bash.Process =
   {
@@ -33,7 +33,8 @@
       else {
         val selection = Sessions.Selection(sessions = List(logic_name))
         val selected_sessions =
-          sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
+          sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
+            .selection(selection)
         selected_sessions.build_requirements(List(logic_name)).
           map(a => File.platform_path(store.heap(a)))
       }