src/Pure/PIDE/resources.scala
changeset 64797 891a25a87ea1
parent 64759 100941134718
child 64823 78df3d65a1cc
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu Jan 05 09:55:26 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Thu Jan 05 10:10:51 2017 +0100
     1.3 @@ -162,6 +162,17 @@
     1.4      else None
     1.5  
     1.6  
     1.7 +  /* blobs */
     1.8 +
     1.9 +  def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
    1.10 +    (for {
    1.11 +      (node_name, node) <- nodes.iterator
    1.12 +      if !loaded_theories(node_name.theory)
    1.13 +      cmd <- node.load_commands.iterator
    1.14 +      name <- cmd.blobs_undefined.iterator
    1.15 +    } yield name).toList
    1.16 +
    1.17 +
    1.18    /* document changes */
    1.19  
    1.20    def parse_change(