src/Pure/General/xml.scala
author wenzelm
Sat Aug 23 11:48:52 2008 +0200 (2008-08-23 ago)
changeset 27948 2638b611d3ce
parent 27947 b6dc0a396857
child 27952 0576c91a6803
permissions -rw-r--r--
renamed DOM to document, add xml version and optional stylesheets;
wenzelm@27931
     1
/*  Title:      Pure/General/xml.scala
wenzelm@27931
     2
    ID:         $Id$
wenzelm@27931
     3
    Author:     Makarius
wenzelm@27931
     4
wenzelm@27947
     5
Simple XML tree values.
wenzelm@27931
     6
*/
wenzelm@27931
     7
wenzelm@27931
     8
package isabelle
wenzelm@27931
     9
wenzelm@27947
    10
import org.w3c.dom.{Node, Document}
wenzelm@27947
    11
import javax.xml.parsers.DocumentBuilderFactory
wenzelm@27947
    12
wenzelm@27947
    13
wenzelm@27931
    14
object XML {
wenzelm@27947
    15
  /* datatype representation */
wenzelm@27947
    16
wenzelm@27931
    17
  type Attributes = List[(String, String)]
wenzelm@27931
    18
wenzelm@27931
    19
  abstract class Tree
wenzelm@27931
    20
  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
wenzelm@27931
    21
  case class Text(content: String) extends Tree
wenzelm@27941
    22
wenzelm@27941
    23
wenzelm@27942
    24
  /* iterate over content */
wenzelm@27941
    25
wenzelm@27941
    26
  private type State = Option[(String, List[Tree])]
wenzelm@27941
    27
wenzelm@27941
    28
  private def get_next(tree: Tree): State = tree match {
wenzelm@27941
    29
    case Elem(_, _, body) => get_nexts(body)
wenzelm@27941
    30
    case Text(content) => Some(content, Nil)
wenzelm@27941
    31
  }
wenzelm@27941
    32
  private def get_nexts(trees: List[Tree]): State = trees match {
wenzelm@27941
    33
    case Nil => None
wenzelm@27941
    34
    case t :: ts => get_next(t) match {
wenzelm@27941
    35
      case None => get_nexts(ts)
wenzelm@27941
    36
      case Some((s, r)) => Some((s, r ::: ts))
wenzelm@27941
    37
    }
wenzelm@27941
    38
  }
wenzelm@27941
    39
wenzelm@27941
    40
  def content(tree: Tree) = new Iterator[String] {
wenzelm@27941
    41
    private var state = get_next(tree)
wenzelm@27941
    42
    def hasNext() = state.isDefined
wenzelm@27941
    43
    def next() = state match {
wenzelm@27941
    44
      case Some((s, rest)) => { state = get_nexts(rest); s }
wenzelm@27941
    45
      case None => throw new NoSuchElementException("next on empty iterator")
wenzelm@27941
    46
    }
wenzelm@27941
    47
  }
wenzelm@27941
    48
wenzelm@27947
    49
wenzelm@27947
    50
  /* document object model (DOM) */
wenzelm@27947
    51
wenzelm@27948
    52
  def document(tree: Tree, styles: String*) = {
wenzelm@27947
    53
    val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
wenzelm@27948
    54
    doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\""))
wenzelm@27948
    55
wenzelm@27948
    56
    for (style <- styles) {
wenzelm@27948
    57
      doc.appendChild(doc.createProcessingInstruction("xml-stylesheet",
wenzelm@27948
    58
        "href=\"" + style + "\" type=\"text/css\""))
wenzelm@27948
    59
    }
wenzelm@27948
    60
wenzelm@27948
    61
    // main body
wenzelm@27947
    62
    def dom_tree(tr: Tree): Node = tr match {
wenzelm@27947
    63
      case Elem(name, atts, ts) => {
wenzelm@27947
    64
        val node = doc.createElement(name)
wenzelm@27947
    65
        for ((name, value) <- atts) node.setAttribute(name, value)
wenzelm@27947
    66
        for (t <- ts) node.appendChild(dom_tree(t))
wenzelm@27947
    67
        node
wenzelm@27947
    68
      }
wenzelm@27947
    69
      case Text(txt) => doc.createTextNode(txt)
wenzelm@27947
    70
    }
wenzelm@27947
    71
    val root_elem = tree match {
wenzelm@27947
    72
      case Elem(_, _, _) => dom_tree(tree)
wenzelm@27947
    73
      case Text(_) => dom_tree(Elem("root", Nil, List(tree)))
wenzelm@27947
    74
    }
wenzelm@27947
    75
    doc.appendChild(root_elem)
wenzelm@27947
    76
    doc
wenzelm@27947
    77
  }
wenzelm@27931
    78
}