src/Pure/General/xml.scala
changeset 27942 5ac9a0f9fad0
parent 27941 b4656b671cce
child 27947 b6dc0a396857
equal deleted inserted replaced
27941:b4656b671cce 27942:5ac9a0f9fad0
    13   abstract class Tree
    13   abstract class Tree
    14   case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
    14   case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
    15   case class Text(content: String) extends Tree
    15   case class Text(content: String) extends Tree
    16 
    16 
    17 
    17 
    18   /* iterator over content */
    18   /* iterate over content */
    19 
    19 
    20   private type State = Option[(String, List[Tree])]
    20   private type State = Option[(String, List[Tree])]
    21 
    21 
    22   private def get_next(tree: Tree): State = tree match {
    22   private def get_next(tree: Tree): State = tree match {
    23     case Elem(_, _, body) => get_nexts(body)
    23     case Elem(_, _, body) => get_nexts(body)