# HG changeset patch
# User wenzelm
# Date 1282222345 -7200
# Node ID 9c1fde4e2487a293dcbc051715449186cfb97aba
# Parent  3d16bebee1d34ec64ae48930b8082b8f6736709b
tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;

diff -r 3d16bebee1d3 -r 9c1fde4e2487 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Thu Aug 19 12:51:48 2010 +0200
+++ b/src/Pure/General/xml.scala	Thu Aug 19 14:52:25 2010 +0200
@@ -67,30 +67,15 @@
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
-  /* iterate over content */
-
-  private type State = Option[(String, List[Tree])]
+  /* text content */
 
-  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_stream(tree: Tree): Stream[String] =
+    tree match {
+      case Elem(_, body) => body.toStream.flatten(content_stream(_))
+      case Text(content) => Stream(content)
     }
-  }
 
-  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")
-    }
-  }
+  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
 
 
   /* pipe-lined cache for partial sharing */