diff -r cda4f24331d5 -r a554da2811f2 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))) }