--- 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)