src/Pure/General/xml.scala
author wenzelm
Thu Dec 10 16:11:07 2009 +0100 (2009-12-10 ago)
changeset 34047 2af94d45597f
parent 34046 8e743ca417b9
child 34108 54d48ca8708f
permissions -rw-r--r--
added get_data;
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@34046
    19
  sealed abstract class Tree {
wenzelm@29204
    20
    override def toString = {
wenzelm@29204
    21
      val s = new StringBuilder
wenzelm@29204
    22
      append_tree(this, s)
wenzelm@29204
    23
      s.toString
wenzelm@29204
    24
    }
wenzelm@29203
    25
  }
wenzelm@29204
    26
  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
wenzelm@29204
    27
  case class Text(content: String) extends Tree
wenzelm@29203
    28
wenzelm@33999
    29
  def elem(name: String, body: List[Tree]) = Elem(name, Nil, body)
wenzelm@33999
    30
  def elem(name: String) = Elem(name, Nil, Nil)
wenzelm@33999
    31
wenzelm@29203
    32
wenzelm@29203
    33
  /* string representation */
wenzelm@29203
    34
wenzelm@29203
    35
  private def append_text(text: String, s: StringBuilder) {
wenzelm@34005
    36
    if (text == null) s ++ text
wenzelm@34005
    37
    else {
wenzelm@34005
    38
      for (c <- text.elements) c match {
wenzelm@34005
    39
        case '<' => s ++ "&lt;"
wenzelm@34005
    40
        case '>' => s ++ "&gt;"
wenzelm@34005
    41
        case '&' => s ++ "&amp;"
wenzelm@34005
    42
        case '"' => s ++ "&quot;"
wenzelm@34005
    43
        case '\'' => s ++ "&apos;"
wenzelm@34005
    44
        case _ => s + c
wenzelm@34005
    45
      }
wenzelm@29203
    46
    }
wenzelm@29203
    47
  }
wenzelm@29203
    48
wenzelm@29203
    49
  private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
wenzelm@34005
    50
    s ++ name
wenzelm@29203
    51
    for ((a, x) <- atts) {
wenzelm@34005
    52
      s ++ " "; s ++ a; s ++ "=\""; append_text(x, s); s ++ "\""
wenzelm@29203
    53
    }
wenzelm@29203
    54
  }
wenzelm@29203
    55
wenzelm@29204
    56
  private def append_tree(tree: Tree, s: StringBuilder) {
wenzelm@29203
    57
    tree match {
wenzelm@29203
    58
      case Elem(name, atts, Nil) =>
wenzelm@34005
    59
        s ++ "<"; append_elem(name, atts, s); s ++ "/>"
wenzelm@29203
    60
      case Elem(name, atts, ts) =>
wenzelm@34005
    61
        s ++ "<"; append_elem(name, atts, s); s ++ ">"
wenzelm@29203
    62
        for (t <- ts) append_tree(t, s)
wenzelm@34005
    63
        s ++ "</"; s ++ name; s ++ ">"
wenzelm@29203
    64
      case Text(text) => append_text(text, s)
wenzelm@29203
    65
    }
wenzelm@29203
    66
  }
wenzelm@27941
    67
wenzelm@27941
    68
wenzelm@27942
    69
  /* iterate over content */
wenzelm@27941
    70
wenzelm@27941
    71
  private type State = Option[(String, List[Tree])]
wenzelm@27941
    72
wenzelm@27941
    73
  private def get_next(tree: Tree): State = tree match {
wenzelm@27941
    74
    case Elem(_, _, body) => get_nexts(body)
wenzelm@27941
    75
    case Text(content) => Some(content, Nil)
wenzelm@27941
    76
  }
wenzelm@27941
    77
  private def get_nexts(trees: List[Tree]): State = trees match {
wenzelm@27941
    78
    case Nil => None
wenzelm@27941
    79
    case t :: ts => get_next(t) match {
wenzelm@27941
    80
      case None => get_nexts(ts)
wenzelm@28007
    81
      case Some((s, r)) => Some((s, r ++ ts))
wenzelm@27941
    82
    }
wenzelm@27941
    83
  }
wenzelm@27941
    84
wenzelm@27941
    85
  def content(tree: Tree) = new Iterator[String] {
wenzelm@27941
    86
    private var state = get_next(tree)
wenzelm@27941
    87
    def hasNext() = state.isDefined
wenzelm@27941
    88
    def next() = state match {
wenzelm@27941
    89
      case Some((s, rest)) => { state = get_nexts(rest); s }
wenzelm@27941
    90
      case None => throw new NoSuchElementException("next on empty iterator")
wenzelm@27941
    91
    }
wenzelm@27941
    92
  }
wenzelm@27941
    93
wenzelm@27947
    94
wenzelm@33953
    95
  /* document object model (W3C DOM) */
wenzelm@27948
    96
wenzelm@34047
    97
  def get_data(node: Node): Option[XML.Tree] =
wenzelm@34047
    98
    node.getUserData(Markup.DATA) match {
wenzelm@34047
    99
      case tree: XML.Tree => Some(tree)
wenzelm@34047
   100
      case _ => None
wenzelm@34047
   101
    }
wenzelm@34047
   102
wenzelm@33953
   103
  def document_node(doc: Document, tree: Tree): Node =
wenzelm@33953
   104
  {
wenzelm@27952
   105
    def DOM(tr: Tree): Node = tr match {
wenzelm@34046
   106
      case Elem(Markup.DATA, Nil, List(data, t)) =>
wenzelm@34046
   107
        val node = DOM(t)
wenzelm@34046
   108
        node.setUserData(Markup.DATA, data, null)
wenzelm@34046
   109
        node
wenzelm@34046
   110
      case Elem(name, atts, ts) =>
wenzelm@34046
   111
        if (name == Markup.DATA)
wenzelm@34046
   112
          error("Malformed data element: " + tr.toString)
wenzelm@27947
   113
        val node = doc.createElement(name)
wenzelm@27947
   114
        for ((name, value) <- atts) node.setAttribute(name, value)
wenzelm@27952
   115
        for (t <- ts) node.appendChild(DOM(t))
wenzelm@27947
   116
        node
wenzelm@27947
   117
      case Text(txt) => doc.createTextNode(txt)
wenzelm@27947
   118
    }
wenzelm@33953
   119
    DOM(tree)
wenzelm@33953
   120
  }
wenzelm@33953
   121
wenzelm@33953
   122
  def document(tree: Tree, styles: String*): Document =
wenzelm@33953
   123
  {
wenzelm@33953
   124
    val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
wenzelm@33953
   125
    doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\""))
wenzelm@33953
   126
wenzelm@33953
   127
    for (style <- styles) {
wenzelm@33953
   128
      doc.appendChild(doc.createProcessingInstruction("xml-stylesheet",
wenzelm@33953
   129
        "href=\"" + style + "\" type=\"text/css\""))
wenzelm@33953
   130
    }
wenzelm@27947
   131
    val root_elem = tree match {
wenzelm@33953
   132
      case Elem(_, _, _) => document_node(doc, tree)
wenzelm@33953
   133
      case Text(_) => document_node(doc, (Elem(Markup.ROOT, Nil, List(tree))))
wenzelm@27947
   134
    }
wenzelm@27947
   135
    doc.appendChild(root_elem)
wenzelm@27947
   136
    doc
wenzelm@27947
   137
  }
wenzelm@27931
   138
}