# HG changeset patch
# User wenzelm
# Date 1510086742 -3600
# Node ID d6d9fd2559ce460ed5cdd527b821ec60e96a9a0c
# Parent  c4e678c2df3c0eba8949bf9cbdc5b3d6b3f09597
clarified signature (again);

diff -r c4e678c2df3c -r d6d9fd2559ce src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 07 17:16:53 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 21:32:22 2017 +0100
@@ -510,6 +510,36 @@
         exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
         session_groups = Library.merge(session_groups, other.session_groups),
         sessions = Library.merge(sessions, other.sessions))
+
+    def selected(graph: Graph[String, Info]): List[String] =
+    {
+      val select_group = session_groups.toSet
+      val select_session = sessions.toSet ++ graph.all_succs(base_sessions)
+
+      val selected0 =
+        if (all_sessions) graph.keys
+        else {
+          (for {
+            (name, (info, _)) <- graph.iterator
+            if info.dir_selected || select_session(name) ||
+              graph.get_node(name).groups.exists(select_group)
+          } yield name).toList
+        }
+
+      if (requirements) (graph.all_preds(selected0).toSet -- selected0).toList
+      else selected0
+    }
+
+    def excluded(graph: Graph[String, Info]): List[String] =
+    {
+      val exclude_group = exclude_session_groups.toSet
+      val exclude_group_sessions =
+        (for {
+          (name, (info, _)) <- graph.iterator
+          if graph.get_node(name).groups.exists(exclude_group)
+        } yield name).toList
+      graph.all_succs(exclude_group_sessions ::: exclude_sessions)
+    }
   }
 
   def make(infos: List[Info]): T =
@@ -584,58 +614,26 @@
       if (bad_sessions.nonEmpty)
         error("Undefined session(s): " + commas_quote(bad_sessions))
 
-      val excluded =
-      {
-        val exclude_group = sel.exclude_session_groups.toSet
-        val exclude_group_sessions =
-          (for {
-            (name, (info, _)) <- build_graph.iterator
-            if build_graph.get_node(name).groups.exists(exclude_group)
-          } yield name).toList
-        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)
+      val excluded = sel.excluded(build_graph).toSet
 
       def restrict(graph: Graph[String, Info]): Graph[String, Info] =
       {
-        val selected0 =
-        {
-          if (sel.all_sessions) graph.keys
-          else {
-            (for {
-              (name, (info, _)) <- graph.iterator
-              if info.dir_selected || select_session(name) || apply(name).groups.exists(select_group)
-            } yield name).toList
-          }
-        }
-
-        val selected1 =
-          if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
-          else selected0
-
-        val selected2 = graph.all_preds(selected1).filterNot(excluded)
-
-        graph.restrict(graph.all_preds(selected2).toSet)
+        val sessions = graph.all_preds(sel.selected(graph)).filterNot(excluded)
+        graph.restrict(graph.all_preds(sessions).toSet)
       }
 
       new T(restrict(build_graph), restrict(imports_graph))
     }
 
-    def build_descendants(names: List[String]): List[String] =
-      build_graph.all_succs(names)
-    def build_requirements(names: List[String]): List[String] =
-      build_graph.all_preds(names).reverse
-    def build_topological_order: List[String] =
-      build_graph.topological_order
+    def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
+    def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
+    def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse
+    def build_topological_order: List[String] = build_graph.topological_order
 
-    def imports_descendants(names: List[String]): List[String] =
-      imports_graph.all_succs(names)
-    def imports_requirements(names: List[String]): List[String] =
-      imports_graph.all_preds(names).reverse
-    def imports_topological_order: List[String] =
-      imports_graph.topological_order
+    def imports_selection(sel: Selection): List[String] = sel.selected(imports_graph)
+    def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
+    def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds(ss).reverse
+    def imports_topological_order: List[String] = imports_graph.topological_order
 
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")