more explicit indication of missing files;
authorwenzelm
Tue Nov 19 22:12:54 2013 +0100 (2013-11-19)
changeset 5452414609d36cab8
parent 54523 11087efad95e
child 54525 de7c13e25212
more explicit indication of missing files;
src/Pure/PIDE/command.scala
src/Pure/PIDE/protocol.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Nov 19 21:49:31 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Nov 19 22:12:54 2013 +0100
     1.3 @@ -144,7 +144,7 @@
     1.4    def name(span: List[Token]): String =
     1.5      span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
     1.6  
     1.7 -  type Blob = Exn.Result[(Document.Node.Name, SHA1.Digest)]
     1.8 +  type Blob = Exn.Result[(Document.Node.Name, Option[SHA1.Digest])]
     1.9  
    1.10    def apply(
    1.11      id: Document_ID.Command,
    1.12 @@ -240,7 +240,7 @@
    1.13    /* blobs */
    1.14  
    1.15    def blobs_digests: List[SHA1.Digest] =
    1.16 -    for (Exn.Res((_, digest)) <- blobs) yield digest
    1.17 +    for (Exn.Res((_, Some(digest))) <- blobs) yield digest
    1.18  
    1.19  
    1.20    /* source */
     2.1 --- a/src/Pure/PIDE/protocol.scala	Tue Nov 19 21:49:31 2013 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Nov 19 22:12:54 2013 +0100
     2.3 @@ -322,8 +322,9 @@
     2.4      { import XML.Encode._
     2.5        val encode_blob: T[Command.Blob] =
     2.6          variant(List(
     2.7 -          { case Exn.Res((a, b)) => (List(a.node, b.toString), Nil) },
     2.8 -          { case Exn.Exn(e) => (List(Exn.message(e)), Nil) }))
     2.9 +          { case Exn.Res((a, Some(b))) => (List(a.node, b.toString), Nil) },
    2.10 +          { case Exn.Res((a, None)) => (List("Missing file: " + quote(a.toString)), Nil)
    2.11 +            case Exn.Exn(e) => (List(Exn.message(e)), Nil) }))
    2.12        YXML.string_of_body(list(encode_blob)(command.blobs))
    2.13      }
    2.14      protocol_command("Document.define_command",
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 21:49:31 2013 +0100
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 22:12:54 2013 +0100
     3.3 @@ -263,10 +263,7 @@
     3.4        Exn.capture {
     3.5          val name =
     3.6            Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
     3.7 -        doc_blobs.get(name) match {
     3.8 -          case Some(blob) => (name, blob.sha1_digest)
     3.9 -          case None => error("No such file: " + quote(name.toString))
    3.10 -        }
    3.11 +        (name, doc_blobs.get(name).map(_.sha1_digest))
    3.12        }
    3.13      )
    3.14    }