tuned;
authorwenzelm
Tue, 07 Nov 2017 17:21:39 +0100
changeset 67027 d4f245bea081
parent 67026 687c822ee5e3
child 67028 c4e678c2df3c
tuned;
src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 07 16:50:26 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 17:21:39 2017 +0100
@@ -595,17 +595,18 @@
         build_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
       }
 
+      val select_group = sel.session_groups.toSet
+      val select_session = sel.sessions.toSet ++ build_graph.all_succs(sel.base_sessions)
+
       def restrict(graph: Graph[String, Info]): Graph[String, Info] =
       {
         val selected0 =
         {
           if (sel.all_sessions) graph.keys
           else {
-            val select_group = sel.session_groups.toSet
-            val select = sel.sessions.toSet ++ build_graph.all_succs(sel.base_sessions)
             (for {
               (name, (info, _)) <- graph.iterator
-              if info.dir_selected || select(name) || apply(name).groups.exists(select_group)
+              if info.dir_selected || select_session(name) || apply(name).groups.exists(select_group)
             } yield name).toList
           }
         }.filterNot(excluded)