src/Pure/General/xml.scala
author wenzelm
Thu Aug 21 19:19:31 2008 +0200 (2008-08-21 ago)
changeset 27941 b4656b671cce
parent 27931 b533a9de87a7
child 27942 5ac9a0f9fad0
permissions -rw-r--r--
added iterator over content;
wenzelm@27931
     1
/*  Title:      Pure/General/xml.scala
wenzelm@27931
     2
    ID:         $Id$
wenzelm@27931
     3
    Author:     Makarius
wenzelm@27931
     4
wenzelm@27931
     5
Minimalistic XML tree values.
wenzelm@27931
     6
*/
wenzelm@27931
     7
wenzelm@27931
     8
package isabelle
wenzelm@27931
     9
wenzelm@27931
    10
object XML {
wenzelm@27931
    11
  type Attributes = List[(String, String)]
wenzelm@27931
    12
wenzelm@27931
    13
  abstract class Tree
wenzelm@27931
    14
  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
wenzelm@27931
    15
  case class Text(content: String) extends Tree
wenzelm@27941
    16
wenzelm@27941
    17
wenzelm@27941
    18
  /* iterator over content */
wenzelm@27941
    19
wenzelm@27941
    20
  private type State = Option[(String, List[Tree])]
wenzelm@27941
    21
wenzelm@27941
    22
  private def get_next(tree: Tree): State = tree match {
wenzelm@27941
    23
    case Elem(_, _, body) => get_nexts(body)
wenzelm@27941
    24
    case Text(content) => Some(content, Nil)
wenzelm@27941
    25
  }
wenzelm@27941
    26
  private def get_nexts(trees: List[Tree]): State = trees match {
wenzelm@27941
    27
    case Nil => None
wenzelm@27941
    28
    case t :: ts => get_next(t) match {
wenzelm@27941
    29
      case None => get_nexts(ts)
wenzelm@27941
    30
      case Some((s, r)) => Some((s, r ::: ts))
wenzelm@27941
    31
    }
wenzelm@27941
    32
  }
wenzelm@27941
    33
wenzelm@27941
    34
  def content(tree: Tree) = new Iterator[String] {
wenzelm@27941
    35
    private var state = get_next(tree)
wenzelm@27941
    36
    def hasNext() = state.isDefined
wenzelm@27941
    37
    def next() = state match {
wenzelm@27941
    38
      case Some((s, rest)) => { state = get_nexts(rest); s }
wenzelm@27941
    39
      case None => throw new NoSuchElementException("next on empty iterator")
wenzelm@27941
    40
    }
wenzelm@27941
    41
  }
wenzelm@27941
    42
wenzelm@27931
    43
}