--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sat Sep 05 00:07:10 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Sat Sep 05 00:15:14 2009 +0200
@@ -69,20 +69,6 @@
}
}
- def dfs: List[MarkupNode] = {
- var all = Nil : List[MarkupNode]
- for (child <- children)
- all = child.dfs ::: all
- all = this :: all
- all
- }
-
- def leafs: List[MarkupNode] =
- {
- if (children.isEmpty) return List(this)
- else return children flatMap (_.leafs)
- }
-
def flatten: List[MarkupNode] = {
var next_x = start
if (children.isEmpty) List(this)