# 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) } }