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