src/Pure/Tools/build.scala
changeset 56372 fadb0fef09d7
parent 56208 06cc31dff138
child 56392 bc118a32a870
     1.1 --- a/src/Pure/Tools/build.scala	Wed Apr 02 18:35:07 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 02 20:22:12 2014 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4              else graph.new_node(name, info)
     1.5          }
     1.6        val graph2 =
     1.7 -        (graph1 /: graph1.entries) {
     1.8 +        (graph1 /: graph1.iterator) {
     1.9            case (graph, (name, (info, _))) =>
    1.10              info.parent match {
    1.11                case None => graph
    1.12 @@ -159,12 +159,12 @@
    1.13  
    1.14        val pre_selected =
    1.15        {
    1.16 -        if (all_sessions) graph.keys.toList
    1.17 +        if (all_sessions) graph.keys
    1.18          else {
    1.19            val select_group = session_groups.toSet
    1.20            val select = sessions.toSet
    1.21            (for {
    1.22 -            (name, (info, _)) <- graph.entries
    1.23 +            (name, (info, _)) <- graph.iterator
    1.24              if info.select || select(name) || apply(name).groups.exists(select_group)
    1.25            } yield name).toList
    1.26          }
    1.27 @@ -180,7 +180,7 @@
    1.28      def topological_order: List[(String, Session_Info)] =
    1.29        graph.topological_order.map(name => (name, apply(name)))
    1.30  
    1.31 -    override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
    1.32 +    override def toString: String = graph.keys_iterator.mkString("Session_Tree(", ", ", ")")
    1.33    }
    1.34  
    1.35  
    1.36 @@ -323,7 +323,7 @@
    1.37      def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
    1.38      {
    1.39        val graph = tree.graph
    1.40 -      val sessions = graph.keys.toList
    1.41 +      val sessions = graph.keys
    1.42  
    1.43        val timings =
    1.44          sessions.par.map((name: String) =>