# HG changeset patch
# User wenzelm
# Date 1406990159 -7200
# Node ID 8e4ae2db184936c08cf12aa88051ce6c82c958cd
# Parent  e212e2001b2a1a19a6b61ed5bd87c01d13a7a68c
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);

diff -r e212e2001b2a -r 8e4ae2db1849 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Aug 02 12:24:30 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Aug 02 16:35:59 2014 +0200
@@ -356,14 +356,14 @@
 
   /* blobs */
 
-  def blobs_changed(doc_blobs: Document.Blobs): Boolean =
-    blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
-
   def blobs_names: List[Document.Node.Name] =
     for (Exn.Res((name, _)) <- blobs) yield name
 
-  def blobs_digests: List[SHA1.Digest] =
-    for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
+  def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] =
+    for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest)
+
+  def blobs_changed(doc_blobs: Document.Blobs): Boolean =
+    blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
 
 
   /* source chunks */
diff -r e212e2001b2a -r 8e4ae2db1849 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Aug 02 12:24:30 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 02 16:35:59 2014 +0200
@@ -58,10 +58,6 @@
 
   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 =
@@ -648,7 +644,7 @@
         (_, node) <- version.nodes.iterator
         command <- node.commands.iterator
       } {
-        for (digest <- command.blobs_digests; if !blobs1.contains(digest))
+        for ((_, digest) <- command.blobs_defined; if !blobs1.contains(digest))
           blobs1 += digest
 
         if (!commands1.isDefinedAt(command.id))
diff -r e212e2001b2a -r 8e4ae2db1849 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Aug 02 12:24:30 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Aug 02 16:35:59 2014 +0200
@@ -47,7 +47,6 @@
 
   sealed case class Change(
     previous: Document.Version,
-    doc_blobs: Document.Blobs,
     syntax_changed: Boolean,
     deps_changed: Boolean,
     doc_edits: List[Document.Edit_Command],
@@ -380,15 +379,15 @@
       def id_command(command: Command)
       {
         for {
-          digest <- command.blobs_digests
+          (name, digest) <- command.blobs_defined
           if !global_state.value.defined_blob(digest)
         } {
-          change.doc_blobs.get(digest) match {
+          change.version.nodes(name).get_blob match {
             case Some(blob) =>
               global_state.change(_.define_blob(digest))
               prover.get.define_blob(digest, blob.bytes)
             case None =>
-              Output.error_message("Missing blob for SHA1 digest " + digest)
+              Output.error_message("Missing blob " + quote(name.toString))
           }
         }
 
diff -r e212e2001b2a -r 8e4ae2db1849 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 02 12:24:30 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 02 16:35:59 2014 +0200
@@ -490,6 +490,6 @@
         (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes))
       }
 
-    Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
+    Session.Change(previous, syntax_changed, deps_changed, doc_edits, version)
   }
 }