| changeset 54517 | 044bee8c5e69 |
| parent 54513 | 5545aff878b1 |
| child 54519 | 5fed81762406 |
--- a/src/Pure/PIDE/command.scala Tue Nov 19 13:13:51 2013 +0100 +++ b/src/Pure/PIDE/command.scala Tue Nov 19 13:39:12 2013 +0100 @@ -144,7 +144,7 @@ def name(span: List[Token]): String = span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" } - type Blobs = List[(Document.Node.Name, Option[SHA1.Digest])] + type Blobs = List[Exn.Result[(Document.Node.Name, SHA1.Digest)]] def apply( id: Document_ID.Command,