tuned signature;
authorwenzelm
Wed Aug 01 19:38:06 2018 +0200 (9 months ago)
changeset 687325472f4409fe6
parent 68731 c2dcb7f7a3ef
child 68733 76e339ef60e3
tuned signature;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Aug 01 16:33:33 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Aug 01 19:38:06 2018 +0200
     1.3 @@ -587,36 +587,6 @@
     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]): Structure =
    1.40 @@ -690,15 +660,43 @@
    1.41          error("Undefined session(s): " + commas_quote(bad_sessions))
    1.42      }
    1.43  
    1.44 +    private def selected(graph: Graph[String, Info], sel: Selection): List[String] =
    1.45 +    {
    1.46 +      val select_group = sel.session_groups.toSet
    1.47 +      val select_session = sel.sessions.toSet ++ graph.all_succs(sel.base_sessions)
    1.48 +
    1.49 +      val selected0 =
    1.50 +        if (sel.all_sessions) graph.keys
    1.51 +        else {
    1.52 +          (for {
    1.53 +            (name, (info, _)) <- graph.iterator
    1.54 +            if info.dir_selected || select_session(name) ||
    1.55 +              graph.get_node(name).groups.exists(select_group)
    1.56 +          } yield name).toList
    1.57 +        }
    1.58 +
    1.59 +      if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
    1.60 +      else selected0
    1.61 +    }
    1.62 +
    1.63      def selection(sel: Selection): Structure =
    1.64      {
    1.65        check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
    1.66  
    1.67 -      val excluded = sel.excluded(build_graph).toSet
    1.68 +      val excluded =
    1.69 +      {
    1.70 +        val exclude_group = sel.exclude_session_groups.toSet
    1.71 +        val exclude_group_sessions =
    1.72 +          (for {
    1.73 +            (name, (info, _)) <- build_graph.iterator
    1.74 +            if build_graph.get_node(name).groups.exists(exclude_group)
    1.75 +          } yield name).toList
    1.76 +        build_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
    1.77 +      }
    1.78  
    1.79        def restrict(graph: Graph[String, Info]): Graph[String, Info] =
    1.80        {
    1.81 -        val sessions = graph.all_preds(sel.selected(graph)).filterNot(excluded)
    1.82 +        val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
    1.83          graph.restrict(graph.all_preds(sessions).toSet)
    1.84        }
    1.85  
    1.86 @@ -714,12 +712,12 @@
    1.87          progress = progress, inlined_files = inlined_files, verbose = verbose)
    1.88      }
    1.89  
    1.90 -    def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
    1.91 +    def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
    1.92      def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
    1.93      def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse
    1.94      def build_topological_order: List[String] = build_graph.topological_order
    1.95  
    1.96 -    def imports_selection(sel: Selection): List[String] = sel.selected(imports_graph)
    1.97 +    def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
    1.98      def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
    1.99      def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds(ss).reverse
   1.100      def imports_topological_order: List[String] = imports_graph.topological_order