# HG changeset patch
# User wenzelm
# Date 1483607451 -3600
# Node ID 891a25a87ea1ef101accf5fc961db73c6dd6b3d6
# Parent  22a1b061ae15bb9459a30e5bbb4e696d8cb9a3c2
tuned;

diff -r 22a1b061ae15 -r 891a25a87ea1 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Jan 05 09:55:26 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Jan 05 10:10:51 2017 +0100
@@ -348,14 +348,6 @@
         if name == file_name
       } yield cmd).toList
 
-    def undefined_blobs(pred: Node.Name => Boolean): List[Node.Name] =
-      (for {
-        (node_name, node) <- iterator
-        if pred(node_name)
-        cmd <- node.load_commands.iterator
-        name <- cmd.blobs_undefined.iterator
-      } yield name).toList
-
     def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
     def topological_order: List[Node.Name] = graph.topological_order
 
diff -r 22a1b061ae15 -r 891a25a87ea1 src/Pure/PIDE/resources.scala
--- 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(
diff -r 22a1b061ae15 -r 891a25a87ea1 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Jan 05 09:55:26 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Jan 05 10:10:51 2017 +0100
@@ -111,9 +111,6 @@
 
   /* theory text edits */
 
-  def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
-    nodes.undefined_blobs(node => !loaded_theories(node.theory))
-
   override def commit(change: Session.Change)
   {
     if (change.syntax_changed.nonEmpty)