/* Title: Pure/General/xml.scala
ID: $Id$
Author: Makarius
Minimalistic XML tree values.
*/
package isabelle
object XML {
type Attributes = List[(String, String)]
abstract class Tree
case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
case class Text(content: String) extends Tree
/* iterate 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")
}
}
}