--- 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",