diff -r 11087efad95e -r 14609d36cab8 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Nov 19 21:49:31 2013 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Nov 19 22:12:54 2013 +0100
@@ -144,7 +144,7 @@
   def name(span: List[Token]): String =
     span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
 
-  type Blob = Exn.Result[(Document.Node.Name, SHA1.Digest)]
+  type Blob = Exn.Result[(Document.Node.Name, Option[SHA1.Digest])]
 
   def apply(
     id: Document_ID.Command,
@@ -240,7 +240,7 @@
   /* blobs */
 
   def blobs_digests: List[SHA1.Digest] =
-    for (Exn.Res((_, digest)) <- blobs) yield digest
+    for (Exn.Res((_, Some(digest))) <- blobs) yield digest
 
 
   /* source */