tuned;
authorwenzelm
Tue Nov 07 17:21:39 2017 +0100 (18 months ago)
changeset 67027d4f245bea081
parent 67026 687c822ee5e3
child 67028 c4e678c2df3c
tuned;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 16:50:26 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 17:21:39 2017 +0100
     1.3 @@ -595,17 +595,18 @@
     1.4          build_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
     1.5        }
     1.6  
     1.7 +      val select_group = sel.session_groups.toSet
     1.8 +      val select_session = sel.sessions.toSet ++ build_graph.all_succs(sel.base_sessions)
     1.9 +
    1.10        def restrict(graph: Graph[String, Info]): Graph[String, Info] =
    1.11        {
    1.12          val selected0 =
    1.13          {
    1.14            if (sel.all_sessions) graph.keys
    1.15            else {
    1.16 -            val select_group = sel.session_groups.toSet
    1.17 -            val select = sel.sessions.toSet ++ build_graph.all_succs(sel.base_sessions)
    1.18              (for {
    1.19                (name, (info, _)) <- graph.iterator
    1.20 -              if info.dir_selected || select(name) || apply(name).groups.exists(select_group)
    1.21 +              if info.dir_selected || select_session(name) || apply(name).groups.exists(select_group)
    1.22              } yield name).toList
    1.23            }
    1.24          }.filterNot(excluded)