1.1 --- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
     1.3 @@ -87,6 +87,12 @@
     1.4      }
     1.5    }
     1.6  
     1.7 +  def filter(p: (MarkupNode => Boolean)): List[MarkupNode] = {
     1.8 +    val filtered = children.flatMap(_.filter(p))
     1.9 +    if (p(this)) List(this set_children(filtered))
    1.10 +    else filtered
    1.11 +  }
    1.12 +
    1.13    def +(new_child : MarkupNode) : MarkupNode = {
    1.14      if (new_child fitting_into this) {
    1.15        val new_children = children.map(c => if((new_child fitting_into c)) c + new_child else c)