| changeset 60916 | a6e2a667b0a8 |
| parent 60215 | 5fb4990dfc73 |
| child 61197 | b9d69001824e |
--- a/src/Pure/PIDE/command.scala Wed Aug 12 03:07:01 2015 +0200 +++ b/src/Pure/PIDE/command.scala Wed Aug 12 13:53:51 2015 +0200 @@ -413,6 +413,9 @@ def blobs_names: List[Document.Node.Name] = for (Exn.Res((name, _)) <- blobs) yield name + def blobs_undefined: List[Document.Node.Name] = + for (Exn.Res((name, None)) <- blobs) yield name + def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest)