changeset 64797 | 891a25a87ea1 |
parent 64759 | 100941134718 |
child 64823 | 78df3d65a1cc |
--- a/src/Pure/PIDE/resources.scala Thu Jan 05 09:55:26 2017 +0100 +++ b/src/Pure/PIDE/resources.scala Thu Jan 05 10:10:51 2017 +0100 @@ -162,6 +162,17 @@ else None + /* blobs */ + + def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = + (for { + (node_name, node) <- nodes.iterator + if !loaded_theories(node_name.theory) + cmd <- node.load_commands.iterator + name <- cmd.blobs_undefined.iterator + } yield name).toList + + /* document changes */ def parse_change(