diff -r 002718f9c938 -r b4656b671cce src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Thu Aug 21 17:42:59 2008 +0200
+++ b/src/Pure/General/xml.scala	Thu Aug 21 19:19:31 2008 +0200
@@ -13,4 +13,31 @@
   abstract class Tree
   case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
   case class Text(content: String) extends Tree
+
+
+  /* iterator over content */
+
+  private type State = Option[(String, List[Tree])]
+
+  private def get_next(tree: Tree): State = tree match {
+    case Elem(_, _, body) => get_nexts(body)
+    case Text(content) => Some(content, Nil)
+  }
+  private def get_nexts(trees: List[Tree]): State = trees match {
+    case Nil => None
+    case t :: ts => get_next(t) match {
+      case None => get_nexts(ts)
+      case Some((s, r)) => Some((s, r ::: ts))
+    }
+  }
+
+  def content(tree: Tree) = new Iterator[String] {
+    private var state = get_next(tree)
+    def hasNext() = state.isDefined
+    def next() = state match {
+      case Some((s, rest)) => { state = get_nexts(rest); s }
+      case None => throw new NoSuchElementException("next on empty iterator")
+    }
+  }
+
 }