src/Pure/PIDE/resources.scala
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(