src/Pure/Thy/sessions.scala
changeset 66848 982baed14542
parent 66843 be08a7691c62
child 66857 f8f42289c4df
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Oct 12 05:37:58 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Oct 12 11:25:06 2017 +0200
     1.3 @@ -509,18 +509,17 @@
     1.4        (selected, new T(build_graph1, imports_graph1))
     1.5      }
     1.6  
     1.7 -    def build_ancestors(name: String): List[String] =
     1.8 -      build_graph.all_preds(List(name)).tail.reverse
     1.9 -
    1.10      def build_descendants(names: List[String]): List[String] =
    1.11        build_graph.all_succs(names)
    1.12 -
    1.13 +    def build_requirements(names: List[String]): List[String] =
    1.14 +      build_graph.all_preds(names).reverse
    1.15      def build_topological_order: List[Info] =
    1.16        build_graph.topological_order.map(apply(_))
    1.17  
    1.18 -    def imports_ancestors(name: String): List[String] =
    1.19 -      imports_graph.all_preds(List(name)).tail.reverse
    1.20 -
    1.21 +    def imports_descendants(names: List[String]): List[String] =
    1.22 +      imports_graph.all_succs(names)
    1.23 +    def imports_requirements(names: List[String]): List[String] =
    1.24 +      imports_graph.all_preds(names).reverse
    1.25      def imports_topological_order: List[Info] =
    1.26        imports_graph.topological_order.map(apply(_))
    1.27