implemented filter on markup-tree

--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
@@ -87,6 +87,12 @@
     }
   }
 
+  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)