# HG changeset patch # User wenzelm # Date 1510071699 -3600 # Node ID d4f245bea0817f9d38c76ebd597871c3ffedd765 # Parent 687c822ee5e36e0600ad51a0b498ae90ce65915a tuned; diff -r 687c822ee5e3 -r d4f245bea081 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)