src/Pure/General/xml.scala
author wenzelm
Thu, 17 Dec 2009 23:31:59 +0100
changeset 34108 54d48ca8708f
parent 34047 2af94d45597f
child 34117 1eb8d8e3e40a
permissions -rw-r--r--
cache for partial sharing;
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
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
     9
import java.util.WeakHashMap
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    10
import java.lang.ref.WeakReference
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    11
import javax.xml.parsers.DocumentBuilderFactory
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    12
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    13
import org.w3c.dom.{Node, Document}
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    14
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    15
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    16
object XML
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    17
{
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    18
  /* datatype representation */
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    19
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
    20
  type Attributes = List[(String, String)]
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
    21
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
    22
  sealed abstract class Tree {
29204
wenzelm
parents: 29203
diff changeset
    23
    override def toString = {
wenzelm
parents: 29203
diff changeset
    24
      val s = new StringBuilder
wenzelm
parents: 29203
diff changeset
    25
      append_tree(this, s)
wenzelm
parents: 29203
diff changeset
    26
      s.toString
wenzelm
parents: 29203
diff changeset
    27
    }
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    28
  }
29204
wenzelm
parents: 29203
diff changeset
    29
  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
wenzelm
parents: 29203
diff changeset
    30
  case class Text(content: String) extends Tree
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    31
33999
d3b200894e21 added auxiliary constructors;
wenzelm
parents: 33953
diff changeset
    32
  def elem(name: String, body: List[Tree]) = Elem(name, Nil, body)
d3b200894e21 added auxiliary constructors;
wenzelm
parents: 33953
diff changeset
    33
  def elem(name: String) = Elem(name, Nil, Nil)
d3b200894e21 added auxiliary constructors;
wenzelm
parents: 33953
diff changeset
    34
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    35
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    36
  /* string representation */
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    37
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    38
  private def append_text(text: String, s: StringBuilder) {
34005
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    39
    if (text == null) s ++ text
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    40
    else {
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    41
      for (c <- text.elements) c match {
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    42
        case '<' => s ++ "&lt;"
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    43
        case '>' => s ++ "&gt;"
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    44
        case '&' => s ++ "&amp;"
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    45
        case '"' => s ++ "&quot;"
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    46
        case '\'' => s ++ "&apos;"
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    47
        case _ => s + c
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    48
      }
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    49
    }
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
  private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
34005
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    53
    s ++ name
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    54
    for ((a, x) <- atts) {
34005
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    55
      s ++ " "; s ++ a; s ++ "=\""; append_text(x, s); s ++ "\""
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    56
    }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    57
  }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    58
29204
wenzelm
parents: 29203
diff changeset
    59
  private def append_tree(tree: Tree, s: StringBuilder) {
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    60
    tree match {
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    61
      case Elem(name, atts, Nil) =>
34005
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    62
        s ++ "<"; append_elem(name, atts, s); s ++ "/>"
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    63
      case Elem(name, atts, ts) =>
34005
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    64
        s ++ "<"; append_elem(name, atts, s); s ++ ">"
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    65
        for (t <- ts) append_tree(t, s)
34005
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    66
        s ++ "</"; s ++ name; s ++ ">"
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    67
      case Text(text) => append_text(text, s)
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    68
    }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    69
  }
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    70
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    71
27942
5ac9a0f9fad0 tuned comment;
wenzelm
parents: 27941
diff changeset
    72
  /* iterate over content */
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    73
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    74
  private type State = Option[(String, List[Tree])]
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    75
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    76
  private def get_next(tree: Tree): State = tree match {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    77
    case Elem(_, _, body) => get_nexts(body)
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    78
    case Text(content) => Some(content, Nil)
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    79
  }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    80
  private def get_nexts(trees: List[Tree]): State = trees match {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    81
    case Nil => None
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    82
    case t :: ts => get_next(t) match {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    83
      case None => get_nexts(ts)
28007
2d0c93291293 tuned append;
wenzelm
parents: 27959
diff changeset
    84
      case Some((s, r)) => Some((s, r ++ ts))
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    85
    }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    86
  }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    87
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    88
  def content(tree: Tree) = new Iterator[String] {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    89
    private var state = get_next(tree)
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    90
    def hasNext() = state.isDefined
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    91
    def next() = state match {
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    92
      case Some((s, rest)) => { state = get_nexts(rest); s }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    93
      case None => throw new NoSuchElementException("next on empty iterator")
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    94
    }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    95
  }
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    96
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    97
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    98
  /* cache for partial sharing -- NOT THREAD SAFE */
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    99
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   100
  class Cache(initial_size: Int)
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   101
  {
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   102
    private val table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   103
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   104
    private def lookup[A](x: A): Option[A] =
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   105
    {
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   106
      val ref = table.get(x)
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   107
      if (ref == null) None
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   108
      else {
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   109
        val y = ref.asInstanceOf[WeakReference[A]].get
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   110
        if (y == null) None
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   111
        else Some(y)
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   112
      }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   113
    }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   114
    private def store[A](x: A): A =
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   115
    {
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   116
      table.put(x, new WeakReference[Any](x))
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   117
      x
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   118
    }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   119
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   120
    def cache_string(x: String): String =
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   121
      lookup(x) match {
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   122
        case Some(y) => y
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   123
        case None => store(x)
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   124
      }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   125
    def cache_props(x: List[(String, String)]): List[(String, String)] =
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   126
      lookup(x) match {
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   127
        case Some(y) => y
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   128
        case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   129
      }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   130
    def apply(x: XML.Tree): XML.Tree =
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   131
      lookup(x) match {
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   132
        case Some(y) => y
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   133
        case None =>
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   134
          x match {
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   135
            case XML.Elem(name, props, body) =>
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   136
              store(XML.Elem(cache_string(name), cache_props(props), apply(body)))
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   137
            case XML.Text(text) => XML.Text(cache_string(text))
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   138
          }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   139
      }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   140
    def apply(x: List[XML.Tree]): List[XML.Tree] =
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   141
      lookup(x) match {
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   142
        case Some(y) => y
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   143
        case None => x.map(apply(_))
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   144
      }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   145
  }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   146
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   147
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   148
  /* document object model (W3C DOM) */
27948
2638b611d3ce renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents: 27947
diff changeset
   149
34047
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   150
  def get_data(node: Node): Option[XML.Tree] =
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   151
    node.getUserData(Markup.DATA) match {
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   152
      case tree: XML.Tree => Some(tree)
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   153
      case _ => None
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   154
    }
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   155
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   156
  def document_node(doc: Document, tree: Tree): Node =
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   157
  {
27952
wenzelm
parents: 27948
diff changeset
   158
    def DOM(tr: Tree): Node = tr match {
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   159
      case Elem(Markup.DATA, Nil, List(data, t)) =>
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   160
        val node = DOM(t)
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   161
        node.setUserData(Markup.DATA, data, null)
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   162
        node
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   163
      case Elem(name, atts, ts) =>
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   164
        if (name == Markup.DATA)
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   165
          error("Malformed data element: " + tr.toString)
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   166
        val node = doc.createElement(name)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   167
        for ((name, value) <- atts) node.setAttribute(name, value)
27952
wenzelm
parents: 27948
diff changeset
   168
        for (t <- ts) node.appendChild(DOM(t))
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   169
        node
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   170
      case Text(txt) => doc.createTextNode(txt)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   171
    }
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   172
    DOM(tree)
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   173
  }
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   174
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   175
  def document(tree: Tree, styles: String*): Document =
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   176
  {
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   177
    val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   178
    doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\""))
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   179
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   180
    for (style <- styles) {
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   181
      doc.appendChild(doc.createProcessingInstruction("xml-stylesheet",
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   182
        "href=\"" + style + "\" type=\"text/css\""))
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   183
    }
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   184
    val root_elem = tree match {
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   185
      case Elem(_, _, _) => document_node(doc, tree)
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   186
      case Text(_) => document_node(doc, (Elem(Markup.ROOT, Nil, List(tree))))
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   187
    }
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   188
    doc.appendChild(root_elem)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   189
    doc
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   190
  }
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
   191
}