src/Pure/Thy/thy_syntax.scala

--- a/src/Pure/Thy/thy_syntax.scala	Tue Feb 11 15:55:05 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Feb 11 17:44:29 2014 +0100
@@ -264,11 +264,16 @@
       doc_blobs: Document.Blobs)
     : List[Command.Blob] =
   {
-    span_files(syntax, span).map(file =>
+    span_files(syntax, span).map(file_name =>
       Exn.capture {
         val name =
-          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
-        (name, doc_blobs.get(name).map(_.sha1_digest))
+          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file_name)))
+        val blob =
+          doc_blobs.get(name) match {
+            case Some((bytes, file)) => Some((bytes.sha1_digest, file))
+            case None => None
+          }
+        (name, blob)
       }
     )
   }