src/Pure/General/xml.scala
author wenzelm
Sun, 06 Dec 2009 22:22:48 +0100
changeset 33999 d3b200894e21
parent 33953 5e865ed88313
child 34005 ada5098506af
permissions -rw-r--r--
added auxiliary constructors;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/xml.scala
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     3
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
     4
Simple XML tree values.
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     5
*/
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     6
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     7
package isabelle
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     8
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
     9
import org.w3c.dom.{Node, Document}
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    10
import javax.xml.parsers.DocumentBuilderFactory
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    11
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    12
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    13
object XML
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    14
{
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    15
  /* datatype representation */
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    16
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
    17
  type Attributes = List[(String, String)]
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
    18
29204
wenzelm
parents: 29203
diff changeset
    19
  abstract class Tree {
wenzelm
parents: 29203
diff changeset
    20
    override def toString = {
wenzelm
parents: 29203
diff changeset
    21
      val s = new StringBuilder
wenzelm
parents: 29203
diff changeset
    22
      append_tree(this, s)
wenzelm
parents: 29203
diff changeset
    23
      s.toString
wenzelm
parents: 29203
diff changeset
    24
    }
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    25
  }
29204
wenzelm
parents: 29203
diff changeset
    26
  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
wenzelm
parents: 29203
diff changeset
    27
  case class Text(content: String) extends Tree
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    28
33999
d3b200894e21 added auxiliary constructors;
wenzelm
parents: 33953
diff changeset
    29
  def elem(name: String, body: List[Tree]) = Elem(name, Nil, body)
d3b200894e21 added auxiliary constructors;
wenzelm
parents: 33953
diff changeset
    30
  def elem(name: String) = Elem(name, Nil, Nil)
d3b200894e21 added auxiliary constructors;
wenzelm
parents: 33953
diff changeset
    31
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    32
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    33
  /* string representation */
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    34
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    35
  private def append_text(text: String, s: StringBuilder) {
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    36
    for (c <- text.elements) c match {
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    37
      case '<' => s.append("&lt;")
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    38
      case '>' => s.append("&gt;")
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    39
      case '&' => s.append("&amp;")
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    40
      case '"' => s.append("&quot;")
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    41
      case '\'' => s.append("&apos;")
29204
wenzelm
parents: 29203
diff changeset
    42
      case _ => s.append(c)
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    43
    }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    44
  }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    45
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    46
  private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    47
    s.append(name)
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    48
    for ((a, x) <- atts) {
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    49
      s.append(" "); s.append(a); s.append("=\""); append_text(x, s); s.append("\"")
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    50
    }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    51
  }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    52
29204
wenzelm
parents: 29203
diff changeset
    53
  private def append_tree(tree: Tree, s: StringBuilder) {
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    54
    tree match {
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    55
      case Elem(name, atts, Nil) =>
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    56
        s.append("<"); append_elem(name, atts, s); s.append("/>")
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    57
      case Elem(name, atts, ts) =>
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    58
        s.append("<"); append_elem(name, atts, s); s.append(">")
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    59
        for (t <- ts) append_tree(t, s)
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    60
        s.append("</"); s.append(name); s.append(">")
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    61
      case Text(text) => append_text(text, s)
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    62
    }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    63
  }
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    64
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    65
27942
5ac9a0f9fad0 tuned comment;
wenzelm
parents: 27941
diff changeset
    66
  /* iterate over content */
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    67
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    68
  private type State = Option[(String, List[Tree])]
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    69
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    70
  private def get_next(tree: Tree): State = tree match {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    71
    case Elem(_, _, body) => get_nexts(body)
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    72
    case Text(content) => Some(content, Nil)
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    73
  }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    74
  private def get_nexts(trees: List[Tree]): State = trees match {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    75
    case Nil => None
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    76
    case t :: ts => get_next(t) match {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    77
      case None => get_nexts(ts)
28007
2d0c93291293 tuned append;
wenzelm
parents: 27959
diff changeset
    78
      case Some((s, r)) => Some((s, r ++ ts))
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    79
    }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    80
  }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    81
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    82
  def content(tree: Tree) = new Iterator[String] {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    83
    private var state = get_next(tree)
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    84
    def hasNext() = state.isDefined
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    85
    def next() = state match {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    86
      case Some((s, rest)) => { state = get_nexts(rest); s }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    87
      case None => throw new NoSuchElementException("next on empty iterator")
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    88
    }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    89
  }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    90
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    91
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
    92
  /* document object model (W3C DOM) */
27948
2638b611d3ce renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents: 27947
diff changeset
    93
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
    94
  def document_node(doc: Document, tree: Tree): Node =
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
    95
  {
27952
wenzelm
parents: 27948
diff changeset
    96
    def DOM(tr: Tree): Node = tr match {
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    97
      case Elem(name, atts, ts) => {
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    98
        val node = doc.createElement(name)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    99
        for ((name, value) <- atts) node.setAttribute(name, value)
27952
wenzelm
parents: 27948
diff changeset
   100
        for (t <- ts) node.appendChild(DOM(t))
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   101
        node
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   102
      }
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   103
      case Text(txt) => doc.createTextNode(txt)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   104
    }
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   105
    DOM(tree)
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   106
  }
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   107
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   108
  def document(tree: Tree, styles: String*): Document =
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   109
  {
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   110
    val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   111
    doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\""))
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   112
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   113
    for (style <- styles) {
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   114
      doc.appendChild(doc.createProcessingInstruction("xml-stylesheet",
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   115
        "href=\"" + style + "\" type=\"text/css\""))
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   116
    }
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   117
    val root_elem = tree match {
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   118
      case Elem(_, _, _) => document_node(doc, tree)
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   119
      case Text(_) => document_node(doc, (Elem(Markup.ROOT, Nil, List(tree))))
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   120
    }
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   121
    doc.appendChild(root_elem)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   122
    doc
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   123
  }
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
   124
}