# HG changeset patch
# User wenzelm
# Date 1384895574 -3600
# Node ID 14609d36cab85d02523c3a3a564d8e9e403bc05e
# Parent  11087efad95eaea7cbae313df1e3d2a0e1e9b75c
more explicit indication of missing files;

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 */
diff -r 11087efad95e -r 14609d36cab8 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Nov 19 21:49:31 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Nov 19 22:12:54 2013 +0100
@@ -322,8 +322,9 @@
     { import XML.Encode._
       val encode_blob: T[Command.Blob] =
         variant(List(
-          { case Exn.Res((a, b)) => (List(a.node, b.toString), Nil) },
-          { case Exn.Exn(e) => (List(Exn.message(e)), Nil) }))
+          { case Exn.Res((a, Some(b))) => (List(a.node, b.toString), Nil) },
+          { case Exn.Res((a, None)) => (List("Missing file: " + quote(a.toString)), Nil)
+            case Exn.Exn(e) => (List(Exn.message(e)), Nil) }))
       YXML.string_of_body(list(encode_blob)(command.blobs))
     }
     protocol_command("Document.define_command",
diff -r 11087efad95e -r 14609d36cab8 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 21:49:31 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 22:12:54 2013 +0100
@@ -263,10 +263,7 @@
       Exn.capture {
         val name =
           Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
-        doc_blobs.get(name) match {
-          case Some(blob) => (name, blob.sha1_digest)
-          case None => error("No such file: " + quote(name.toString))
-        }
+        (name, doc_blobs.get(name).map(_.sha1_digest))
       }
     )
   }