tuned;
authorwenzelm
Thu, 05 Jan 2017 10:10:51 +0100
changeset 64797 891a25a87ea1
parent 64796 22a1b061ae15
child 64798 0e5ec80c352a
tuned;
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
src/Tools/jEdit/src/jedit_resources.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
 
--- 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(
--- 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)