src/Pure/ML/ml_process.scala
changeset 68204 a554da2811f2
parent 67586 8b19a8a7f029
child 68209 aeffd8f1f079
     1.1 --- a/src/Pure/ML/ml_process.scala	Thu May 17 14:50:48 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_process.scala	Thu May 17 15:38:36 2018 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4      redirect: Boolean = false,
     1.5      cleanup: () => Unit = () => (),
     1.6      channel: Option[System_Channel] = None,
     1.7 -    sessions: Option[Sessions.Structure] = None,
     1.8 +    sessions_structure: Option[Sessions.Structure] = None,
     1.9      session_base: Option[Sessions.Base] = None,
    1.10      store: Sessions.Store = Sessions.store()): Bash.Process =
    1.11    {
    1.12 @@ -33,7 +33,8 @@
    1.13        else {
    1.14          val selection = Sessions.Selection(sessions = List(logic_name))
    1.15          val selected_sessions =
    1.16 -          sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
    1.17 +          sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
    1.18 +            .selection(selection)
    1.19          selected_sessions.build_requirements(List(logic_name)).
    1.20            map(a => File.platform_path(store.heap(a)))
    1.21        }