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