src/Pure/General/xml.scala
author wenzelm
Wed Aug 11 00:42:01 2010 +0200 (2010-08-11 ago)
changeset 38268 beb86b805590
parent 38267 e50c283dd125
child 38446 9d59dab38fef
permissions -rw-r--r--
more uniform XML/YXML string_of_body/string_of_tree;
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@34108
     9
import java.util.WeakHashMap
wenzelm@34108
    10
import java.lang.ref.WeakReference
wenzelm@34108
    11
import javax.xml.parsers.DocumentBuilderFactory
wenzelm@34108
    12
wenzelm@27947
    13
wenzelm@29203
    14
object XML
wenzelm@29203
    15
{
wenzelm@27947
    16
  /* datatype representation */
wenzelm@27947
    17
wenzelm@27931
    18
  type Attributes = List[(String, String)]
wenzelm@27931
    19
wenzelm@38268
    20
  sealed abstract class Tree { override def toString = string_of_tree(this) }
wenzelm@38230
    21
  case class Elem(markup: Markup, body: List[Tree]) extends Tree
wenzelm@29204
    22
  case class Text(content: String) extends Tree
wenzelm@29203
    23
wenzelm@38230
    24
  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
wenzelm@38230
    25
  def elem(name: String) = Elem(Markup(name, Nil), Nil)
wenzelm@33999
    26
wenzelm@38267
    27
  type Body = List[Tree]
wenzelm@38267
    28
wenzelm@29203
    29
wenzelm@29203
    30
  /* string representation */
wenzelm@29203
    31
wenzelm@38268
    32
  def string_of_body(body: Body): String =
wenzelm@38268
    33
  {
wenzelm@38268
    34
    val s = new StringBuilder
wenzelm@38268
    35
wenzelm@38268
    36
    def text(txt: String) {
wenzelm@38268
    37
      if (txt == null) s ++= txt
wenzelm@38268
    38
      else {
wenzelm@38268
    39
        for (c <- txt.iterator) c match {
wenzelm@38268
    40
          case '<' => s ++= "&lt;"
wenzelm@38268
    41
          case '>' => s ++= "&gt;"
wenzelm@38268
    42
          case '&' => s ++= "&amp;"
wenzelm@38268
    43
          case '"' => s ++= "&quot;"
wenzelm@38268
    44
          case '\'' => s ++= "&apos;"
wenzelm@38268
    45
          case _ => s += c
wenzelm@38268
    46
        }
wenzelm@34005
    47
      }
wenzelm@29203
    48
    }
wenzelm@38268
    49
    def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
wenzelm@38268
    50
    def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
wenzelm@38268
    51
    def tree(t: Tree): Unit =
wenzelm@38268
    52
      t match {
wenzelm@38268
    53
        case Elem(markup, Nil) =>
wenzelm@38268
    54
          s ++= "<"; elem(markup); s ++= "/>"
wenzelm@38268
    55
        case Elem(markup, ts) =>
wenzelm@38268
    56
          s ++= "<"; elem(markup); s ++= ">"
wenzelm@38268
    57
          ts.foreach(tree)
wenzelm@38268
    58
          s ++= "</"; s ++= markup.name; s ++= ">"
wenzelm@38268
    59
        case Text(txt) => text(txt)
wenzelm@38268
    60
      }
wenzelm@38268
    61
    body.foreach(tree)
wenzelm@38268
    62
    s.toString
wenzelm@29203
    63
  }
wenzelm@29203
    64
wenzelm@38268
    65
  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
wenzelm@27941
    66
wenzelm@27941
    67
wenzelm@27942
    68
  /* iterate over content */
wenzelm@27941
    69
wenzelm@27941
    70
  private type State = Option[(String, List[Tree])]
wenzelm@27941
    71
wenzelm@27941
    72
  private def get_next(tree: Tree): State = tree match {
wenzelm@38230
    73
    case Elem(_, body) => get_nexts(body)
wenzelm@27941
    74
    case Text(content) => Some(content, Nil)
wenzelm@27941
    75
  }
wenzelm@27941
    76
  private def get_nexts(trees: List[Tree]): State = trees match {
wenzelm@27941
    77
    case Nil => None
wenzelm@27941
    78
    case t :: ts => get_next(t) match {
wenzelm@27941
    79
      case None => get_nexts(ts)
wenzelm@28007
    80
      case Some((s, r)) => Some((s, r ++ ts))
wenzelm@27941
    81
    }
wenzelm@27941
    82
  }
wenzelm@27941
    83
wenzelm@27941
    84
  def content(tree: Tree) = new Iterator[String] {
wenzelm@27941
    85
    private var state = get_next(tree)
wenzelm@27941
    86
    def hasNext() = state.isDefined
wenzelm@27941
    87
    def next() = state match {
wenzelm@27941
    88
      case Some((s, rest)) => { state = get_nexts(rest); s }
wenzelm@27941
    89
      case None => throw new NoSuchElementException("next on empty iterator")
wenzelm@27941
    90
    }
wenzelm@27941
    91
  }
wenzelm@27941
    92
wenzelm@27947
    93
wenzelm@34108
    94
  /* cache for partial sharing -- NOT THREAD SAFE */
wenzelm@34108
    95
wenzelm@34108
    96
  class Cache(initial_size: Int)
wenzelm@34108
    97
  {
wenzelm@34108
    98
    private val table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
wenzelm@34108
    99
wenzelm@34108
   100
    private def lookup[A](x: A): Option[A] =
wenzelm@34108
   101
    {
wenzelm@34108
   102
      val ref = table.get(x)
wenzelm@34108
   103
      if (ref == null) None
wenzelm@34108
   104
      else {
wenzelm@34108
   105
        val y = ref.asInstanceOf[WeakReference[A]].get
wenzelm@34108
   106
        if (y == null) None
wenzelm@34108
   107
        else Some(y)
wenzelm@34108
   108
      }
wenzelm@34108
   109
    }
wenzelm@34108
   110
    private def store[A](x: A): A =
wenzelm@34108
   111
    {
wenzelm@34108
   112
      table.put(x, new WeakReference[Any](x))
wenzelm@34108
   113
      x
wenzelm@34108
   114
    }
wenzelm@34108
   115
wenzelm@34108
   116
    def cache_string(x: String): String =
wenzelm@34108
   117
      lookup(x) match {
wenzelm@34108
   118
        case Some(y) => y
wenzelm@38233
   119
        case None => store(new String(x.toCharArray))  // trim string value
wenzelm@34108
   120
      }
wenzelm@34108
   121
    def cache_props(x: List[(String, String)]): List[(String, String)] =
wenzelm@34133
   122
      if (x.isEmpty) x
wenzelm@34133
   123
      else
wenzelm@34133
   124
        lookup(x) match {
wenzelm@34133
   125
          case Some(y) => y
wenzelm@34133
   126
          case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
wenzelm@34133
   127
        }
wenzelm@38230
   128
    def cache_markup(x: Markup): Markup =
wenzelm@38230
   129
      lookup(x) match {
wenzelm@38230
   130
        case Some(y) => y
wenzelm@38230
   131
        case None =>
wenzelm@38230
   132
          x match {
wenzelm@38230
   133
            case Markup(name, props) =>
wenzelm@38230
   134
              store(Markup(cache_string(name), cache_props(props)))
wenzelm@38230
   135
          }
wenzelm@38230
   136
      }
wenzelm@34117
   137
    def cache_tree(x: XML.Tree): XML.Tree =
wenzelm@34108
   138
      lookup(x) match {
wenzelm@34108
   139
        case Some(y) => y
wenzelm@34108
   140
        case None =>
wenzelm@34108
   141
          x match {
wenzelm@38230
   142
            case XML.Elem(markup, body) =>
wenzelm@38230
   143
              store(XML.Elem(cache_markup(markup), cache_trees(body)))
wenzelm@38230
   144
            case XML.Text(text) => store(XML.Text(cache_string(text)))
wenzelm@34108
   145
          }
wenzelm@34108
   146
      }
wenzelm@34117
   147
    def cache_trees(x: List[XML.Tree]): List[XML.Tree] =
wenzelm@34133
   148
      if (x.isEmpty) x
wenzelm@34133
   149
      else
wenzelm@34133
   150
        lookup(x) match {
wenzelm@34133
   151
          case Some(y) => y
wenzelm@34133
   152
          case None => x.map(cache_tree(_))
wenzelm@34133
   153
        }
wenzelm@34108
   154
  }
wenzelm@34108
   155
wenzelm@34108
   156
wenzelm@33953
   157
  /* document object model (W3C DOM) */
wenzelm@27948
   158
wenzelm@34871
   159
  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
wenzelm@38231
   160
    node.getUserData(Markup.Data.name) match {
wenzelm@34047
   161
      case tree: XML.Tree => Some(tree)
wenzelm@34047
   162
      case _ => None
wenzelm@34047
   163
    }
wenzelm@34047
   164
wenzelm@34871
   165
  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
wenzelm@33953
   166
  {
wenzelm@34871
   167
    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
wenzelm@38231
   168
      case Elem(Markup.Data, List(data, t)) =>
wenzelm@34046
   169
        val node = DOM(t)
wenzelm@38231
   170
        node.setUserData(Markup.Data.name, data, null)
wenzelm@34046
   171
        node
wenzelm@38230
   172
      case Elem(Markup(name, atts), ts) =>
wenzelm@38231
   173
        if (name == Markup.Data.name)
wenzelm@34046
   174
          error("Malformed data element: " + tr.toString)
wenzelm@27947
   175
        val node = doc.createElement(name)
wenzelm@27947
   176
        for ((name, value) <- atts) node.setAttribute(name, value)
wenzelm@27952
   177
        for (t <- ts) node.appendChild(DOM(t))
wenzelm@27947
   178
        node
wenzelm@27947
   179
      case Text(txt) => doc.createTextNode(txt)
wenzelm@27947
   180
    }
wenzelm@33953
   181
    DOM(tree)
wenzelm@33953
   182
  }
wenzelm@27931
   183
}