src/Pure/PIDE/document.scala
changeset 55801 28b59620f0d0
parent 55800 d3c9fa520689
child 55820 61869776ce1f
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Feb 28 11:50:54 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Feb 28 11:58:26 2014 +0100
     1.3 @@ -55,6 +55,10 @@
     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 @@ -63,9 +67,6 @@
    1.15          case None => false
    1.16        }
    1.17  
    1.18 -    def retrieve(digest: SHA1.Digest): Option[Blob] =
    1.19 -      blobs.collectFirst({ case (_, blob) if blob.bytes.sha1_digest == digest => blob })
    1.20 -
    1.21      override def toString: String = blobs.mkString("Blobs(", ",", ")")
    1.22    }
    1.23