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