src/Pure/PIDE/document.scala
changeset 55783 da0513d95155
parent 55782 47ed6a67a304
child 55800 d3c9fa520689
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Feb 27 12:48:59 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Feb 27 14:07:04 2014 +0100
     1.3 @@ -43,14 +43,39 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* individual nodes */
     1.8 +  /* document blobs: auxiliary files */
     1.9 +
    1.10 +  sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
    1.11 +
    1.12 +  object Blobs
    1.13 +  {
    1.14 +    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
    1.15 +    val empty: Blobs = apply(Map.empty)
    1.16 +  }
    1.17 +
    1.18 +  final class Blobs private(blobs: Map[Node.Name, Blob])
    1.19 +  {
    1.20 +    override def toString: String = blobs.mkString("Blobs(", ",", ")")
    1.21 +
    1.22 +    def get(name: Node.Name): Option[Blob] = blobs.get(name)
    1.23 +
    1.24 +    def changed(name: Node.Name): Boolean =
    1.25 +      get(name) match {
    1.26 +        case Some(blob) => blob.changed
    1.27 +        case None => false
    1.28 +      }
    1.29 +
    1.30 +    def retrieve(digest: SHA1.Digest): Option[Blob] =
    1.31 +      blobs.collectFirst({ case (_, blob) if blob.bytes.sha1_digest == digest => blob })
    1.32 +  }
    1.33 +
    1.34 +
    1.35 +  /* document nodes: theories and auxiliary files */
    1.36  
    1.37    type Edit[A, B] = (Node.Name, Node.Edit[A, B])
    1.38    type Edit_Text = Edit[Text.Edit, Text.Perspective]
    1.39    type Edit_Command = Edit[Command.Edit, Command.Perspective]
    1.40  
    1.41 -  type Blobs = Map[Node.Name, (Bytes, Command.File)]
    1.42 -
    1.43    object Node
    1.44    {
    1.45      val empty: Node = new Node()