tuned;
authorwenzelm
Thu Jan 05 10:10:51 2017 +0100 (2017-01-05 ago)
changeset 64797891a25a87ea1
parent 64796 22a1b061ae15
child 64798 0e5ec80c352a
tuned;
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Jan 05 09:55:26 2017 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Jan 05 10:10:51 2017 +0100
     1.3 @@ -348,14 +348,6 @@
     1.4          if name == file_name
     1.5        } yield cmd).toList
     1.6  
     1.7 -    def undefined_blobs(pred: Node.Name => Boolean): List[Node.Name] =
     1.8 -      (for {
     1.9 -        (node_name, node) <- iterator
    1.10 -        if pred(node_name)
    1.11 -        cmd <- node.load_commands.iterator
    1.12 -        name <- cmd.blobs_undefined.iterator
    1.13 -      } yield name).toList
    1.14 -
    1.15      def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
    1.16      def topological_order: List[Node.Name] = graph.topological_order
    1.17  
     2.1 --- a/src/Pure/PIDE/resources.scala	Thu Jan 05 09:55:26 2017 +0100
     2.2 +++ b/src/Pure/PIDE/resources.scala	Thu Jan 05 10:10:51 2017 +0100
     2.3 @@ -162,6 +162,17 @@
     2.4      else None
     2.5  
     2.6  
     2.7 +  /* blobs */
     2.8 +
     2.9 +  def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
    2.10 +    (for {
    2.11 +      (node_name, node) <- nodes.iterator
    2.12 +      if !loaded_theories(node_name.theory)
    2.13 +      cmd <- node.load_commands.iterator
    2.14 +      name <- cmd.blobs_undefined.iterator
    2.15 +    } yield name).toList
    2.16 +
    2.17 +
    2.18    /* document changes */
    2.19  
    2.20    def parse_change(
     3.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Jan 05 09:55:26 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Jan 05 10:10:51 2017 +0100
     3.3 @@ -111,9 +111,6 @@
     3.4  
     3.5    /* theory text edits */
     3.6  
     3.7 -  def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
     3.8 -    nodes.undefined_blobs(node => !loaded_theories(node.theory))
     3.9 -
    3.10    override def commit(change: Session.Change)
    3.11    {
    3.12      if (change.syntax_changed.nonEmpty)