src/Pure/PIDE/document.scala
changeset 57842 8e4ae2db1849
parent 57621 caa37976801f
child 57976 bf99106b6672
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 02 12:24:30 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 02 16:35:59 2014 +0200
     1.3 @@ -58,10 +58,6 @@
     1.4  
     1.5    final class Blobs private(blobs: Map[Node.Name, Blob])
     1.6    {
     1.7 -    private lazy val digests: Map[SHA1.Digest, Blob] =
     1.8 -      for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob)
     1.9 -
    1.10 -    def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest)
    1.11      def get(name: Node.Name): Option[Blob] = blobs.get(name)
    1.12  
    1.13      def changed(name: Node.Name): Boolean =
    1.14 @@ -648,7 +644,7 @@
    1.15          (_, node) <- version.nodes.iterator
    1.16          command <- node.commands.iterator
    1.17        } {
    1.18 -        for (digest <- command.blobs_digests; if !blobs1.contains(digest))
    1.19 +        for ((_, digest) <- command.blobs_defined; if !blobs1.contains(digest))
    1.20            blobs1 += digest
    1.21  
    1.22          if (!commands1.isDefinedAt(command.id))