src/Pure/PIDE/command.scala
changeset 54530 2c1440f70028
parent 54524 14609d36cab8
child 55429 4a50f9e70dc1
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Nov 20 15:00:25 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Nov 20 15:53:59 2013 +0100
     1.3 @@ -239,6 +239,9 @@
     1.4  
     1.5    /* blobs */
     1.6  
     1.7 +  def blobs_names: List[Document.Node.Name] =
     1.8 +    for (Exn.Res((name, _)) <- blobs) yield name
     1.9 +
    1.10    def blobs_digests: List[SHA1.Digest] =
    1.11      for (Exn.Res((_, Some(digest))) <- blobs) yield digest
    1.12