# HG changeset patch
# User wenzelm
# Date 1393585106 -3600
# Node ID 28b59620f0d096064a181fe7f79ddc05b2a5756b
# Parent  d3c9fa5206893359cf5f70a618d1b59de7c783c0
tuned data structure;

diff -r d3c9fa520689 -r 28b59620f0d0 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Feb 28 11:50:54 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Feb 28 11:58:26 2014 +0100
@@ -55,6 +55,10 @@
 
   final class Blobs private(blobs: Map[Node.Name, Blob])
   {
+    private lazy val digests: Map[SHA1.Digest, Blob] =
+      for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob)
+
+    def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest)
     def get(name: Node.Name): Option[Blob] = blobs.get(name)
 
     def changed(name: Node.Name): Boolean =
@@ -63,9 +67,6 @@
         case None => false
       }
 
-    def retrieve(digest: SHA1.Digest): Option[Blob] =
-      blobs.collectFirst({ case (_, blob) if blob.bytes.sha1_digest == digest => blob })
-
     override def toString: String = blobs.mkString("Blobs(", ",", ")")
   }
 
diff -r d3c9fa520689 -r 28b59620f0d0 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Feb 28 11:50:54 2014 +0100
+++ b/src/Pure/System/session.scala	Fri Feb 28 11:58:26 2014 +0100
@@ -378,7 +378,7 @@
           digest <- command.blobs_digests
           if !global_state().defined_blob(digest)
         } {
-          doc_blobs.retrieve(digest) match {
+          doc_blobs.get(digest) match {
             case Some(blob) =>
               global_state >> (_.define_blob(digest))
               prover.get.define_blob(blob)