# HG changeset patch
# User wenzelm
# Date 1252102514 -7200
# Node ID cce1dcc923dc42137694853134756946c5a3b871
# Parent  cd2cdf3b33b9eb8490821145e61c017d721811c8
removed dead code;

diff -r cd2cdf3b33b9 -r cce1dcc923dc src/Tools/jEdit/src/prover/MarkupNode.scala
--- 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)