clarified signature (again);
authorwenzelm
Tue Nov 07 21:32:22 2017 +0100 (13 months ago)
changeset 67029d6d9fd2559ce
parent 67028 c4e678c2df3c
child 67030 a9859e879f38
clarified signature (again);
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 17:16:53 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 21:32:22 2017 +0100
     1.3 @@ -510,6 +510,36 @@
     1.4          exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
     1.5          session_groups = Library.merge(session_groups, other.session_groups),
     1.6          sessions = Library.merge(sessions, other.sessions))
     1.7 +
     1.8 +    def selected(graph: Graph[String, Info]): List[String] =
     1.9 +    {
    1.10 +      val select_group = session_groups.toSet
    1.11 +      val select_session = sessions.toSet ++ graph.all_succs(base_sessions)
    1.12 +
    1.13 +      val selected0 =
    1.14 +        if (all_sessions) graph.keys
    1.15 +        else {
    1.16 +          (for {
    1.17 +            (name, (info, _)) <- graph.iterator
    1.18 +            if info.dir_selected || select_session(name) ||
    1.19 +              graph.get_node(name).groups.exists(select_group)
    1.20 +          } yield name).toList
    1.21 +        }
    1.22 +
    1.23 +      if (requirements) (graph.all_preds(selected0).toSet -- selected0).toList
    1.24 +      else selected0
    1.25 +    }
    1.26 +
    1.27 +    def excluded(graph: Graph[String, Info]): List[String] =
    1.28 +    {
    1.29 +      val exclude_group = exclude_session_groups.toSet
    1.30 +      val exclude_group_sessions =
    1.31 +        (for {
    1.32 +          (name, (info, _)) <- graph.iterator
    1.33 +          if graph.get_node(name).groups.exists(exclude_group)
    1.34 +        } yield name).toList
    1.35 +      graph.all_succs(exclude_group_sessions ::: exclude_sessions)
    1.36 +    }
    1.37    }
    1.38  
    1.39    def make(infos: List[Info]): T =
    1.40 @@ -584,58 +614,26 @@
    1.41        if (bad_sessions.nonEmpty)
    1.42          error("Undefined session(s): " + commas_quote(bad_sessions))
    1.43  
    1.44 -      val excluded =
    1.45 -      {
    1.46 -        val exclude_group = sel.exclude_session_groups.toSet
    1.47 -        val exclude_group_sessions =
    1.48 -          (for {
    1.49 -            (name, (info, _)) <- build_graph.iterator
    1.50 -            if build_graph.get_node(name).groups.exists(exclude_group)
    1.51 -          } yield name).toList
    1.52 -        build_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
    1.53 -      }
    1.54 -
    1.55 -      val select_group = sel.session_groups.toSet
    1.56 -      val select_session = sel.sessions.toSet ++ build_graph.all_succs(sel.base_sessions)
    1.57 +      val excluded = sel.excluded(build_graph).toSet
    1.58  
    1.59        def restrict(graph: Graph[String, Info]): Graph[String, Info] =
    1.60        {
    1.61 -        val selected0 =
    1.62 -        {
    1.63 -          if (sel.all_sessions) graph.keys
    1.64 -          else {
    1.65 -            (for {
    1.66 -              (name, (info, _)) <- graph.iterator
    1.67 -              if info.dir_selected || select_session(name) || apply(name).groups.exists(select_group)
    1.68 -            } yield name).toList
    1.69 -          }
    1.70 -        }
    1.71 -
    1.72 -        val selected1 =
    1.73 -          if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
    1.74 -          else selected0
    1.75 -
    1.76 -        val selected2 = graph.all_preds(selected1).filterNot(excluded)
    1.77 -
    1.78 -        graph.restrict(graph.all_preds(selected2).toSet)
    1.79 +        val sessions = graph.all_preds(sel.selected(graph)).filterNot(excluded)
    1.80 +        graph.restrict(graph.all_preds(sessions).toSet)
    1.81        }
    1.82  
    1.83        new T(restrict(build_graph), restrict(imports_graph))
    1.84      }
    1.85  
    1.86 -    def build_descendants(names: List[String]): List[String] =
    1.87 -      build_graph.all_succs(names)
    1.88 -    def build_requirements(names: List[String]): List[String] =
    1.89 -      build_graph.all_preds(names).reverse
    1.90 -    def build_topological_order: List[String] =
    1.91 -      build_graph.topological_order
    1.92 +    def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
    1.93 +    def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
    1.94 +    def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse
    1.95 +    def build_topological_order: List[String] = build_graph.topological_order
    1.96  
    1.97 -    def imports_descendants(names: List[String]): List[String] =
    1.98 -      imports_graph.all_succs(names)
    1.99 -    def imports_requirements(names: List[String]): List[String] =
   1.100 -      imports_graph.all_preds(names).reverse
   1.101 -    def imports_topological_order: List[String] =
   1.102 -      imports_graph.topological_order
   1.103 +    def imports_selection(sel: Selection): List[String] = sel.selected(imports_graph)
   1.104 +    def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
   1.105 +    def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds(ss).reverse
   1.106 +    def imports_topological_order: List[String] = imports_graph.topological_order
   1.107  
   1.108      override def toString: String =
   1.109        imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")