src/Pure/PIDE/xml.scala
author wenzelm
Wed Sep 07 23:08:04 2011 +0200 (2011-09-07 ago)
changeset 44808 05b8997899a2
parent 44721 ba478c3f7255
child 45667 546d78f0d81f
permissions -rw-r--r--
XML.cache for partial sharing (strings only);
     1 /*  Title:      Pure/PIDE/xml.scala
     2     Author:     Makarius
     3 
     4 Untyped XML trees and basic data representation.
     5 */
     6 
     7 package isabelle
     8 
     9 import java.lang.System
    10 import java.util.WeakHashMap
    11 import java.lang.ref.WeakReference
    12 import javax.xml.parsers.DocumentBuilderFactory
    13 
    14 import scala.collection.mutable
    15 
    16 
    17 object XML
    18 {
    19   /** XML trees **/
    20 
    21   /* datatype representation */
    22 
    23   type Attributes = Properties.T
    24 
    25   sealed abstract class Tree { override def toString = string_of_tree(this) }
    26   case class Elem(markup: Markup, body: List[Tree]) extends Tree
    27   case class Text(content: String) extends Tree
    28 
    29   def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
    30   def elem(name: String) = Elem(Markup(name, Nil), Nil)
    31 
    32   type Body = List[Tree]
    33 
    34 
    35   /* string representation */
    36 
    37   def string_of_body(body: Body): String =
    38   {
    39     val s = new StringBuilder
    40 
    41     def text(txt: String) {
    42       if (txt == null) s ++= txt
    43       else {
    44         for (c <- txt.iterator) c match {
    45           case '<' => s ++= "&lt;"
    46           case '>' => s ++= "&gt;"
    47           case '&' => s ++= "&amp;"
    48           case '"' => s ++= "&quot;"
    49           case '\'' => s ++= "&apos;"
    50           case _ => s += c
    51         }
    52       }
    53     }
    54     def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
    55     def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
    56     def tree(t: Tree): Unit =
    57       t match {
    58         case Elem(markup, Nil) =>
    59           s ++= "<"; elem(markup); s ++= "/>"
    60         case Elem(markup, ts) =>
    61           s ++= "<"; elem(markup); s ++= ">"
    62           ts.foreach(tree)
    63           s ++= "</"; s ++= markup.name; s ++= ">"
    64         case Text(txt) => text(txt)
    65       }
    66     body.foreach(tree)
    67     s.toString
    68   }
    69 
    70   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
    71 
    72 
    73   /* text content */
    74 
    75   def content_stream(tree: Tree): Stream[String] =
    76     tree match {
    77       case Elem(_, body) => content_stream(body)
    78       case Text(content) => Stream(content)
    79     }
    80   def content_stream(body: Body): Stream[String] =
    81     body.toStream.flatten(content_stream(_))
    82 
    83   def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
    84   def content(body: Body): Iterator[String] = content_stream(body).iterator
    85 
    86 
    87 
    88   /** cache for partial sharing (weak table) **/
    89 
    90   class Cache(initial_size: Int = 131071, max_string: Int = 100)
    91   {
    92     private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
    93 
    94     private def lookup[A](x: A): Option[A] =
    95     {
    96       val ref = table.get(x)
    97       if (ref == null) None
    98       else {
    99         val y = ref.asInstanceOf[WeakReference[A]].get
   100         if (y == null) None
   101         else Some(y)
   102       }
   103     }
   104     private def store[A](x: A): A =
   105     {
   106       table.put(x, new WeakReference[Any](x))
   107       x
   108     }
   109 
   110     private def trim_bytes(s: String): String = new String(s.toCharArray)
   111 
   112     private def _cache_string(x: String): String =
   113       lookup(x) match {
   114         case Some(y) => y
   115         case None =>
   116           val z = trim_bytes(x)
   117           if (z.length > max_string) z else store(z)
   118       }
   119     private def _cache_props(x: Properties.T): Properties.T =
   120       if (x.isEmpty) x
   121       else
   122         lookup(x) match {
   123           case Some(y) => y
   124           case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
   125         }
   126     private def _cache_markup(x: Markup): Markup =
   127       lookup(x) match {
   128         case Some(y) => y
   129         case None =>
   130           x match {
   131             case Markup(name, props) =>
   132               store(Markup(_cache_string(name), _cache_props(props)))
   133           }
   134       }
   135     private def _cache_tree(x: XML.Tree): XML.Tree =
   136       lookup(x) match {
   137         case Some(y) => y
   138         case None =>
   139           x match {
   140             case XML.Elem(markup, body) =>
   141               store(XML.Elem(_cache_markup(markup), _cache_body(body)))
   142             case XML.Text(text) => store(XML.Text(_cache_string(text)))
   143           }
   144       }
   145     private def _cache_body(x: XML.Body): XML.Body =
   146       if (x.isEmpty) x
   147       else
   148         lookup(x) match {
   149           case Some(y) => y
   150           case None => x.map(_cache_tree(_))
   151         }
   152 
   153     // main methods
   154     def cache_string(x: String): String = synchronized { _cache_string(x) }
   155     def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
   156     def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
   157     def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
   158   }
   159 
   160 
   161 
   162   /** document object model (W3C DOM) **/
   163 
   164   def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
   165     node.getUserData(Markup.Data.name) match {
   166       case tree: XML.Tree => Some(tree)
   167       case _ => None
   168     }
   169 
   170   def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
   171   {
   172     def DOM(tr: Tree): org.w3c.dom.Node = tr match {
   173       case Elem(Markup.Data, List(data, t)) =>
   174         val node = DOM(t)
   175         node.setUserData(Markup.Data.name, data, null)
   176         node
   177       case Elem(Markup(name, atts), ts) =>
   178         if (name == Markup.Data.name)
   179           error("Malformed data element: " + tr.toString)
   180         val node = doc.createElement(name)
   181         for ((name, value) <- atts) node.setAttribute(name, value)
   182         for (t <- ts) node.appendChild(DOM(t))
   183         node
   184       case Text(txt) => doc.createTextNode(txt)
   185     }
   186     DOM(tree)
   187   }
   188 
   189 
   190 
   191   /** XML as data representation language **/
   192 
   193   class XML_Atom(s: String) extends Exception(s)
   194   class XML_Body(body: XML.Body) extends Exception
   195 
   196   object Encode
   197   {
   198     type T[A] = A => XML.Body
   199 
   200 
   201     /* atomic values */
   202 
   203     def long_atom(i: Long): String = i.toString
   204 
   205     def int_atom(i: Int): String = i.toString
   206 
   207     def bool_atom(b: Boolean): String = if (b) "1" else "0"
   208 
   209     def unit_atom(u: Unit) = ""
   210 
   211 
   212     /* structural nodes */
   213 
   214     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
   215 
   216     private def vector(xs: List[String]): XML.Attributes =
   217       xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
   218 
   219     private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
   220       XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
   221 
   222 
   223     /* representation of standard types */
   224 
   225     val properties: T[Properties.T] =
   226       (props => List(XML.Elem(Markup(":", props), Nil)))
   227 
   228     val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
   229 
   230     val long: T[Long] = (x => string(long_atom(x)))
   231 
   232     val int: T[Int] = (x => string(int_atom(x)))
   233 
   234     val bool: T[Boolean] = (x => string(bool_atom(x)))
   235 
   236     val unit: T[Unit] = (x => string(unit_atom(x)))
   237 
   238     def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   239       (x => List(node(f(x._1)), node(g(x._2))))
   240 
   241     def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   242       (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
   243 
   244     def list[A](f: T[A]): T[List[A]] =
   245       (xs => xs.map((x: A) => node(f(x))))
   246 
   247     def option[A](f: T[A]): T[Option[A]] =
   248     {
   249       case None => Nil
   250       case Some(x) => List(node(f(x)))
   251     }
   252 
   253     def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
   254     {
   255       case x =>
   256         val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
   257         List(tagged(tag, f(x)))
   258     }
   259   }
   260 
   261   object Decode
   262   {
   263     type T[A] = XML.Body => A
   264     type V[A] = (List[String], XML.Body) => A
   265 
   266 
   267     /* atomic values */
   268 
   269     def long_atom(s: String): Long =
   270       try { java.lang.Long.parseLong(s) }
   271       catch { case e: NumberFormatException => throw new XML_Atom(s) }
   272 
   273     def int_atom(s: String): Int =
   274       try { Integer.parseInt(s) }
   275       catch { case e: NumberFormatException => throw new XML_Atom(s) }
   276 
   277     def bool_atom(s: String): Boolean =
   278       if (s == "1") true
   279       else if (s == "0") false
   280       else throw new XML_Atom(s)
   281 
   282     def unit_atom(s: String): Unit =
   283       if (s == "") () else throw new XML_Atom(s)
   284 
   285 
   286     /* structural nodes */
   287 
   288     private def node(t: XML.Tree): XML.Body =
   289       t match {
   290         case XML.Elem(Markup(":", Nil), ts) => ts
   291         case _ => throw new XML_Body(List(t))
   292       }
   293 
   294     private def vector(atts: XML.Attributes): List[String] =
   295     {
   296       val xs = new mutable.ListBuffer[String]
   297       var i = 0
   298       for ((a, x) <- atts) {
   299         if (int_atom(a) == i) { xs += x; i = i + 1 }
   300         else throw new XML_Atom(a)
   301       }
   302       xs.toList
   303     }
   304 
   305     private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
   306       t match {
   307         case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
   308         case _ => throw new XML_Body(List(t))
   309       }
   310 
   311 
   312     /* representation of standard types */
   313 
   314     val properties: T[Properties.T] =
   315     {
   316       case List(XML.Elem(Markup(":", props), Nil)) => props
   317       case ts => throw new XML_Body(ts)
   318     }
   319 
   320     val string: T[String] =
   321     {
   322       case Nil => ""
   323       case List(XML.Text(s)) => s
   324       case ts => throw new XML_Body(ts)
   325     }
   326 
   327     val long: T[Long] = (x => long_atom(string(x)))
   328 
   329     val int: T[Int] = (x => int_atom(string(x)))
   330 
   331     val bool: T[Boolean] = (x => bool_atom(string(x)))
   332 
   333     val unit: T[Unit] = (x => unit_atom(string(x)))
   334 
   335     def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   336     {
   337       case List(t1, t2) => (f(node(t1)), g(node(t2)))
   338       case ts => throw new XML_Body(ts)
   339     }
   340 
   341     def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   342     {
   343       case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
   344       case ts => throw new XML_Body(ts)
   345     }
   346 
   347     def list[A](f: T[A]): T[List[A]] =
   348       (ts => ts.map(t => f(node(t))))
   349 
   350     def option[A](f: T[A]): T[Option[A]] =
   351     {
   352       case Nil => None
   353       case List(t) => Some(f(node(t)))
   354       case ts => throw new XML_Body(ts)
   355     }
   356 
   357     def variant[A](fs: List[V[A]]): T[A] =
   358     {
   359       case List(t) =>
   360         val (tag, (xs, ts)) = tagged(t)
   361         val f =
   362           try { fs(tag) }
   363           catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
   364         f(xs, ts)
   365       case ts => throw new XML_Body(ts)
   366     }
   367   }
   368 }