src/Tools/jEdit/src/prover/MarkupNode.scala

       if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, desc)
       else filled_gaps
     }
   }
 
+  def filter(p: (MarkupNode => Boolean)): List[MarkupNode] = {
+    val filtered = children.flatMap(_.filter(p))
+    if (p(this)) List(this set_children(filtered))
+    else filtered
+  }
+
   def +(new_child : MarkupNode) : MarkupNode = {
     if (new_child fitting_into this) {
       val new_children = children.map(c => if((new_child fitting_into c)) c + new_child else c)
       if (new_children == children) {
         // new_child did not fit into children of this -> insert new_child between this and its children