src/Pure/Thy/sessions.scala
changeset 67023 e27e05d6f2a7
parent 67018 f6aa133f9b16
child 67024 72d37a2e9cca
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 11:11:37 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 15:45:33 2017 +0100
     1.3 @@ -204,9 +204,10 @@
     1.4  
     1.5      val session_bases =
     1.6        (Map.empty[String, Base] /: sessions.imports_topological_order)({
     1.7 -        case (session_bases, info) =>
     1.8 +        case (session_bases, session_name) =>
     1.9            if (progress.stopped) throw Exn.Interrupt()
    1.10  
    1.11 +          val info = sessions(session_name)
    1.12            try {
    1.13              val parent_base: Sessions.Base =
    1.14                info.parent match {
    1.15 @@ -624,15 +625,15 @@
    1.16        build_graph.all_succs(names)
    1.17      def build_requirements(names: List[String]): List[String] =
    1.18        build_graph.all_preds(names).reverse
    1.19 -    def build_topological_order: List[Info] =
    1.20 -      build_graph.topological_order.map(apply(_))
    1.21 +    def build_topological_order: List[String] =
    1.22 +      build_graph.topological_order
    1.23  
    1.24      def imports_descendants(names: List[String]): List[String] =
    1.25        imports_graph.all_succs(names)
    1.26      def imports_requirements(names: List[String]): List[String] =
    1.27        imports_graph.all_preds(names).reverse
    1.28 -    def imports_topological_order: List[Info] =
    1.29 -      imports_graph.topological_order.map(apply(_))
    1.30 +    def imports_topological_order: List[String] =
    1.31 +      imports_graph.topological_order
    1.32  
    1.33      override def toString: String =
    1.34        imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")