src/Pure/PIDE/document.scala
changeset 56372 fadb0fef09d7
parent 56354 a6f8c3566560
child 56373 0605d90be6fc
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Apr 02 18:35:07 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Apr 02 20:22:12 2014 +0200
     1.3 @@ -274,7 +274,7 @@
     1.4    final class Nodes private(graph: Graph[Node.Name, Node])
     1.5    {
     1.6      def get_name(s: String): Option[Node.Name] =
     1.7 -      graph.keys.find(name => name.node == s)
     1.8 +      graph.keys_iterator.find(name => name.node == s)
     1.9  
    1.10      def apply(name: Node.Name): Node =
    1.11        graph.default_node(name, Node.empty).get_node(name)
    1.12 @@ -290,12 +290,12 @@
    1.13        new Nodes(graph3.map_node(name, _ => node))
    1.14      }
    1.15  
    1.16 -    def entries: Iterator[(Node.Name, Node)] =
    1.17 -      graph.entries.map({ case (name, (node, _)) => (name, node) })
    1.18 +    def iterator: Iterator[(Node.Name, Node)] =
    1.19 +      graph.iterator.map({ case (name, (node, _)) => (name, node) })
    1.20  
    1.21      def load_commands(file_name: Node.Name): List[Command] =
    1.22        (for {
    1.23 -        (_, node) <- entries
    1.24 +        (_, node) <- iterator
    1.25          cmd <- node.load_commands.iterator
    1.26          name <- cmd.blobs_names.iterator
    1.27          if name == file_name
    1.28 @@ -617,7 +617,7 @@
    1.29        for {
    1.30          (version_id, version) <- versions1.iterator
    1.31          command_execs = assignments1(version_id).command_execs
    1.32 -        (_, node) <- version.nodes.entries
    1.33 +        (_, node) <- version.nodes.iterator
    1.34          command <- node.commands.iterator
    1.35        } {
    1.36          for (digest <- command.blobs_digests; if !blobs1.contains(digest))