src/Pure/General/xml.scala
author wenzelm
Mon Dec 29 22:20:04 2008 +0100 (2008-12-29 ago)
changeset 29203 0c4effb73518
parent 29140 e7ac5bb20aed
child 29204 e002f7b63e3c
permissions -rw-r--r--
override toString method;
wenzelm@27931
     1
/*  Title:      Pure/General/xml.scala
wenzelm@27931
     2
    Author:     Makarius
wenzelm@27931
     3
wenzelm@27947
     4
Simple XML tree values.
wenzelm@27931
     5
*/
wenzelm@27931
     6
wenzelm@27931
     7
package isabelle
wenzelm@27931
     8
wenzelm@27947
     9
import org.w3c.dom.{Node, Document}
wenzelm@27947
    10
import javax.xml.parsers.DocumentBuilderFactory
wenzelm@27947
    11
wenzelm@27947
    12
wenzelm@29203
    13
object XML
wenzelm@29203
    14
{
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@29203
    20
  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree {
wenzelm@29203
    21
    override def toString = append_tree(this, new StringBuilder).toString
wenzelm@29203
    22
  }
wenzelm@29203
    23
  case class Text(content: String) extends Tree {
wenzelm@29203
    24
    override def toString = append_tree(this, new StringBuilder).toString
wenzelm@29203
    25
  }
wenzelm@29203
    26
wenzelm@29203
    27
wenzelm@29203
    28
  /* string representation */
wenzelm@29203
    29
wenzelm@29203
    30
  private def append_text(text: String, s: StringBuilder) {
wenzelm@29203
    31
    for (c <- text.elements) c match {
wenzelm@29203
    32
      case '<' => s.append("&lt;")
wenzelm@29203
    33
      case '>' => s.append("&gt;")
wenzelm@29203
    34
      case '&' => s.append("&amp;")
wenzelm@29203
    35
      case '"' => s.append("&quot;")
wenzelm@29203
    36
      case '\'' => s.append("&apos;")
wenzelm@29203
    37
      case _   => s.append(c)
wenzelm@29203
    38
    }
wenzelm@29203
    39
  }
wenzelm@29203
    40
wenzelm@29203
    41
  private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
wenzelm@29203
    42
    s.append(name)
wenzelm@29203
    43
    for ((a, x) <- atts) {
wenzelm@29203
    44
      s.append(" "); s.append(a); s.append("=\""); append_text(x, s); s.append("\"")
wenzelm@29203
    45
    }
wenzelm@29203
    46
  }
wenzelm@29203
    47
wenzelm@29203
    48
  private def append_tree(tree: Tree, s: StringBuilder): StringBuilder = {
wenzelm@29203
    49
    tree match {
wenzelm@29203
    50
      case Elem(name, atts, Nil) =>
wenzelm@29203
    51
        s.append("<"); append_elem(name, atts, s); s.append("/>")
wenzelm@29203
    52
      case Elem(name, atts, ts) =>
wenzelm@29203
    53
        s.append("<"); append_elem(name, atts, s); s.append(">")
wenzelm@29203
    54
        for (t <- ts) append_tree(t, s)
wenzelm@29203
    55
        s.append("</"); s.append(name); s.append(">")
wenzelm@29203
    56
      case Text(text) => append_text(text, s)
wenzelm@29203
    57
    }
wenzelm@29203
    58
    s
wenzelm@29203
    59
  }
wenzelm@27941
    60
wenzelm@27941
    61
wenzelm@27942
    62
  /* iterate over content */
wenzelm@27941
    63
wenzelm@27941
    64
  private type State = Option[(String, List[Tree])]
wenzelm@27941
    65
wenzelm@27941
    66
  private def get_next(tree: Tree): State = tree match {
wenzelm@27941
    67
    case Elem(_, _, body) => get_nexts(body)
wenzelm@27941
    68
    case Text(content) => Some(content, Nil)
wenzelm@27941
    69
  }
wenzelm@27941
    70
  private def get_nexts(trees: List[Tree]): State = trees match {
wenzelm@27941
    71
    case Nil => None
wenzelm@27941
    72
    case t :: ts => get_next(t) match {
wenzelm@27941
    73
      case None => get_nexts(ts)
wenzelm@28007
    74
      case Some((s, r)) => Some((s, r ++ ts))
wenzelm@27941
    75
    }
wenzelm@27941
    76
  }
wenzelm@27941
    77
wenzelm@27941
    78
  def content(tree: Tree) = new Iterator[String] {
wenzelm@27941
    79
    private var state = get_next(tree)
wenzelm@27941
    80
    def hasNext() = state.isDefined
wenzelm@27941
    81
    def next() = state match {
wenzelm@27941
    82
      case Some((s, rest)) => { state = get_nexts(rest); s }
wenzelm@27941
    83
      case None => throw new NoSuchElementException("next on empty iterator")
wenzelm@27941
    84
    }
wenzelm@27941
    85
  }
wenzelm@27941
    86
wenzelm@27947
    87
wenzelm@27947
    88
  /* document object model (DOM) */
wenzelm@27947
    89
wenzelm@27948
    90
  def document(tree: Tree, styles: String*) = {
wenzelm@27947
    91
    val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
wenzelm@27948
    92
    doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\""))
wenzelm@27948
    93
wenzelm@27948
    94
    for (style <- styles) {
wenzelm@27948
    95
      doc.appendChild(doc.createProcessingInstruction("xml-stylesheet",
wenzelm@27948
    96
        "href=\"" + style + "\" type=\"text/css\""))
wenzelm@27948
    97
    }
wenzelm@27948
    98
wenzelm@27948
    99
    // main body
wenzelm@27952
   100
    def DOM(tr: Tree): Node = tr match {
wenzelm@27947
   101
      case Elem(name, atts, ts) => {
wenzelm@27947
   102
        val node = doc.createElement(name)
wenzelm@27947
   103
        for ((name, value) <- atts) node.setAttribute(name, value)
wenzelm@27952
   104
        for (t <- ts) node.appendChild(DOM(t))
wenzelm@27947
   105
        node
wenzelm@27947
   106
      }
wenzelm@27947
   107
      case Text(txt) => doc.createTextNode(txt)
wenzelm@27947
   108
    }
wenzelm@27947
   109
    val root_elem = tree match {
wenzelm@27952
   110
      case Elem(_, _, _) => DOM(tree)
wenzelm@27959
   111
      case Text(_) => DOM(Elem(Markup.ROOT, Nil, List(tree)))
wenzelm@27947
   112
    }
wenzelm@27947
   113
    doc.appendChild(root_elem)
wenzelm@27947
   114
    doc
wenzelm@27947
   115
  }
wenzelm@27931
   116
}