src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Feb 27 14:07:04 2014 +0100
@@ -43,14 +43,39 @@
   }
 
 
-  /* individual nodes */
+  /* document blobs: auxiliary files */
+
+  sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
+
+  object Blobs
+  {
+    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
+    val empty: Blobs = apply(Map.empty)
+  }
+
+  final class Blobs private(blobs: Map[Node.Name, Blob])
+  {
+    override def toString: String = blobs.mkString("Blobs(", ",", ")")
+
+    def get(name: Node.Name): Option[Blob] = blobs.get(name)
+
+    def changed(name: Node.Name): Boolean =
+      get(name) match {
+        case Some(blob) => blob.changed
+        case None => false
+      }
+
+    def retrieve(digest: SHA1.Digest): Option[Blob] =
+      blobs.collectFirst({ case (_, blob) if blob.bytes.sha1_digest == digest => blob })
+  }
+
+
+  /* document nodes: theories and auxiliary files */
 
   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
-  type Blobs = Map[Node.Name, (Bytes, Command.File)]
-
   object Node
   {
     val empty: Node = new Node()