# HG changeset patch
# User immler@in.tum.de
# Date 1242992614 -7200
# Node ID 2adb23c3e5d1d0ac7198aad54ccb5973c0baa77c
# Parent  668fae39d86d06d2fdc15b3c6b96cbe7c970886d
implemented filter on markup-tree

diff -r 668fae39d86d -r 2adb23c3e5d1 src/Tools/jEdit/src/prover/MarkupNode.scala
--- 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)