more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
authorwenzelm
Sat Aug 02 16:35:59 2014 +0200 (2014-08-02)
changeset 578428e4ae2db1849
parent 57841 e212e2001b2a
child 57843 d8966c09025c
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Aug 02 12:24:30 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Aug 02 16:35:59 2014 +0200
     1.3 @@ -356,14 +356,14 @@
     1.4  
     1.5    /* blobs */
     1.6  
     1.7 -  def blobs_changed(doc_blobs: Document.Blobs): Boolean =
     1.8 -    blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
     1.9 -
    1.10    def blobs_names: List[Document.Node.Name] =
    1.11      for (Exn.Res((name, _)) <- blobs) yield name
    1.12  
    1.13 -  def blobs_digests: List[SHA1.Digest] =
    1.14 -    for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
    1.15 +  def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] =
    1.16 +    for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest)
    1.17 +
    1.18 +  def blobs_changed(doc_blobs: Document.Blobs): Boolean =
    1.19 +    blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
    1.20  
    1.21  
    1.22    /* source chunks */
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 02 12:24:30 2014 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 02 16:35:59 2014 +0200
     2.3 @@ -58,10 +58,6 @@
     2.4  
     2.5    final class Blobs private(blobs: Map[Node.Name, Blob])
     2.6    {
     2.7 -    private lazy val digests: Map[SHA1.Digest, Blob] =
     2.8 -      for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob)
     2.9 -
    2.10 -    def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest)
    2.11      def get(name: Node.Name): Option[Blob] = blobs.get(name)
    2.12  
    2.13      def changed(name: Node.Name): Boolean =
    2.14 @@ -648,7 +644,7 @@
    2.15          (_, node) <- version.nodes.iterator
    2.16          command <- node.commands.iterator
    2.17        } {
    2.18 -        for (digest <- command.blobs_digests; if !blobs1.contains(digest))
    2.19 +        for ((_, digest) <- command.blobs_defined; if !blobs1.contains(digest))
    2.20            blobs1 += digest
    2.21  
    2.22          if (!commands1.isDefinedAt(command.id))
     3.1 --- a/src/Pure/PIDE/session.scala	Sat Aug 02 12:24:30 2014 +0200
     3.2 +++ b/src/Pure/PIDE/session.scala	Sat Aug 02 16:35:59 2014 +0200
     3.3 @@ -47,7 +47,6 @@
     3.4  
     3.5    sealed case class Change(
     3.6      previous: Document.Version,
     3.7 -    doc_blobs: Document.Blobs,
     3.8      syntax_changed: Boolean,
     3.9      deps_changed: Boolean,
    3.10      doc_edits: List[Document.Edit_Command],
    3.11 @@ -380,15 +379,15 @@
    3.12        def id_command(command: Command)
    3.13        {
    3.14          for {
    3.15 -          digest <- command.blobs_digests
    3.16 +          (name, digest) <- command.blobs_defined
    3.17            if !global_state.value.defined_blob(digest)
    3.18          } {
    3.19 -          change.doc_blobs.get(digest) match {
    3.20 +          change.version.nodes(name).get_blob match {
    3.21              case Some(blob) =>
    3.22                global_state.change(_.define_blob(digest))
    3.23                prover.get.define_blob(digest, blob.bytes)
    3.24              case None =>
    3.25 -              Output.error_message("Missing blob for SHA1 digest " + digest)
    3.26 +              Output.error_message("Missing blob " + quote(name.toString))
    3.27            }
    3.28          }
    3.29  
     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 02 12:24:30 2014 +0200
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 02 16:35:59 2014 +0200
     4.3 @@ -490,6 +490,6 @@
     4.4          (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes))
     4.5        }
     4.6  
     4.7 -    Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
     4.8 +    Session.Change(previous, syntax_changed, deps_changed, doc_edits, version)
     4.9    }
    4.10  }