src/Pure/PIDE/markup_tree.scala
changeset 38576 ce3eed2b16f7
parent 38571 f7d7b8054648
child 38577 4e4d3ea3725a
equal deleted inserted replaced
38575:80d962964216 38576:ce3eed2b16f7
    86           }
    86           }
    87         }
    87         }
    88     }
    88     }
    89   }
    89   }
    90 
    90 
    91   // FIXME depth-first with result markup stack
       
    92   // FIXME projection to given range
       
    93   def flatten(parent: Node[Any]): List[Node[Any]] =
       
    94   {
       
    95     val result = new mutable.ListBuffer[Node[Any]]
       
    96     var offset = parent.range.start
       
    97     for ((_, (node, subtree)) <- branches.iterator) {
       
    98       if (offset < node.range.start)
       
    99         result += new Node(Text.Range(offset, node.range.start), parent.info)
       
   100       result ++= subtree.flatten(node)
       
   101       offset = node.range.stop
       
   102     }
       
   103     if (offset < parent.range.stop)
       
   104       result += new Node(Text.Range(offset, parent.range.stop), parent.info)
       
   105     result.toList
       
   106   }
       
   107 
       
   108   def filter(pred: Node[Any] => Boolean): Markup_Tree =
       
   109   {
       
   110     val bs = branches.toList.flatMap(entry => {
       
   111       val (_, (node, subtree)) = entry
       
   112       if (pred(node)) List((node, (node, subtree.filter(pred))))
       
   113       else subtree.filter(pred).branches.toList
       
   114     })
       
   115     new Markup_Tree(Branches.empty ++ bs)
       
   116   }
       
   117 
       
   118   def select[A](root: Node[A])(sel: PartialFunction[Any, A]): Stream[Node[A]] =
    91   def select[A](root: Node[A])(sel: PartialFunction[Any, A]): Stream[Node[A]] =
   119   {
    92   {
   120     def stream(parent: Node[A], bs: Branches.T): Stream[Node[A]] =
    93     def stream(parent: Node[A], bs: Branches.T): Stream[Node[A]] =
   121     {
    94     {
   122       val substream =
    95       val substream =