src/Pure/Tools/build.scala

               error("Duplicate session " + quote(name) + Position.here(info.pos) +
                 Position.here(graph.get_node(name).pos))
             else graph.new_node(name, info)
         }
       val graph2 =
-        (graph1 /: graph1.entries) {
+        (graph1 /: graph1.iterator) {
           case (graph, (name, (info, _))) =>
             info.parent match {
               case None => graph
               case Some(parent) =>
                 if (!graph.defined(parent))

       val bad_sessions = sessions.filterNot(isDefinedAt(_))
       if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
 
       val pre_selected =
       {
-        if (all_sessions) graph.keys.toList
+        if (all_sessions) graph.keys
         else {
           val select_group = session_groups.toSet
           val select = sessions.toSet
           (for {
-            (name, (info, _)) <- graph.entries
+            (name, (info, _)) <- graph.iterator
             if info.select || select(name) || apply(name).groups.exists(select_group)
           } yield name).toList
         }
       }
       val selected =

     }
 
     def topological_order: List[(String, Session_Info)] =
       graph.topological_order.map(name => (name, apply(name)))
 
-    override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
+    override def toString: String = graph.keys_iterator.mkString("Session_Tree(", ", ", ")")
   }
 
 
   /* parser */
 

   object Queue
   {
     def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
     {
       val graph = tree.graph
-      val sessions = graph.keys.toList
+      val sessions = graph.keys
 
       val timings =
         sessions.par.map((name: String) =>
           Exn.capture { (name, load_timings(name)) }).toList.map(Exn.release(_))
       val command_timings =