tuned data structure;
authorwenzelm
Fri Feb 28 11:58:26 2014 +0100 (2014-02-28)
changeset 5580128b59620f0d0
parent 55800 d3c9fa520689
child 55802 f7ceebe2f1b5
tuned data structure;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     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  
     2.1 --- a/src/Pure/System/session.scala	Fri Feb 28 11:50:54 2014 +0100
     2.2 +++ b/src/Pure/System/session.scala	Fri Feb 28 11:58:26 2014 +0100
     2.3 @@ -378,7 +378,7 @@
     2.4            digest <- command.blobs_digests
     2.5            if !global_state().defined_blob(digest)
     2.6          } {
     2.7 -          doc_blobs.retrieve(digest) match {
     2.8 +          doc_blobs.get(digest) match {
     2.9              case Some(blob) =>
    2.10                global_state >> (_.define_blob(digest))
    2.11                prover.get.define_blob(blob)