src/Pure/PIDE/xml.scala
author wenzelm
Tue Feb 19 20:19:21 2013 +0100 (2013-02-19 ago)
changeset 51223 c6a8a05ff0a0
parent 49650 9fad6480300d
child 51663 098f3cf6c809
permissions -rw-r--r--
help JVM to cope with large symbolic structures;
     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.util.WeakHashMap
    11 import java.lang.ref.WeakReference
    12 import javax.xml.parsers.DocumentBuilderFactory
    13 
    14 
    15 object XML
    16 {
    17   /** XML trees **/
    18 
    19   /* datatype representation */
    20 
    21   type Attributes = Properties.T
    22 
    23   sealed abstract class Tree { override def toString = string_of_tree(this) }
    24   case class Elem(markup: Markup, body: List[Tree]) extends Tree
    25   case class Text(content: String) extends Tree
    26 
    27   def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
    28   def elem(name: String) = Elem(Markup(name, Nil), Nil)
    29 
    30   type Body = List[Tree]
    31 
    32 
    33   /* wrapped elements */
    34 
    35   val XML_ELEM = "xml_elem";
    36   val XML_NAME = "xml_name";
    37   val XML_BODY = "xml_body";
    38 
    39   object Wrapped_Elem
    40   {
    41     def apply(markup: Markup, body1: Body, body2: Body): XML.Elem =
    42       Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
    43         Elem(Markup(XML_BODY, Nil), body1) :: body2)
    44 
    45     def unapply(tree: Tree): Option[(Markup, Body, Body)] =
    46       tree match {
    47         case
    48           Elem(Markup(XML_ELEM, (XML_NAME, name) :: props),
    49             Elem(Markup(XML_BODY, Nil), body1) :: body2) =>
    50           Some(Markup(name, props), body1, body2)
    51         case _ => None
    52       }
    53   }
    54 
    55 
    56   /* traverse text */
    57 
    58   def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
    59   {
    60     def traverse(x: A, t: Tree): A =
    61       t match {
    62         case Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
    63         case Elem(_, ts) => (x /: ts)(traverse)
    64         case Text(s) => op(x, s)
    65       }
    66     (a /: body)(traverse)
    67   }
    68 
    69   def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
    70 
    71 
    72   /* text content */
    73 
    74   def content(body: Body): String =
    75   {
    76     val text = new StringBuilder(text_length(body))
    77     traverse_text(body)(()) { case (_, s) => text.append(s) }
    78     text.toString
    79   }
    80 
    81   def content(tree: Tree): String = content(List(tree))
    82 
    83 
    84 
    85   /** string representation **/
    86 
    87   def string_of_body(body: Body): String =
    88   {
    89     val s = new StringBuilder
    90 
    91     def text(txt: String) {
    92       if (txt == null) s ++= txt
    93       else {
    94         for (c <- txt.iterator) c match {
    95           case '<' => s ++= "&lt;"
    96           case '>' => s ++= "&gt;"
    97           case '&' => s ++= "&amp;"
    98           case '"' => s ++= "&quot;"
    99           case '\'' => s ++= "&apos;"
   100           case _ => s += c
   101         }
   102       }
   103     }
   104     def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
   105     def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
   106     def tree(t: Tree): Unit =
   107       t match {
   108         case Elem(markup, Nil) =>
   109           s ++= "<"; elem(markup); s ++= "/>"
   110         case Elem(markup, ts) =>
   111           s ++= "<"; elem(markup); s ++= ">"
   112           ts.foreach(tree)
   113           s ++= "</"; s ++= markup.name; s ++= ">"
   114         case Text(txt) => text(txt)
   115       }
   116     body.foreach(tree)
   117     s.toString
   118   }
   119 
   120   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
   121 
   122 
   123 
   124   /** cache for partial sharing (weak table) **/
   125 
   126   class Cache(initial_size: Int = 131071, max_string: Int = 100)
   127   {
   128     private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
   129 
   130     private def lookup[A](x: A): Option[A] =
   131     {
   132       val ref = table.get(x)
   133       if (ref == null) None
   134       else {
   135         val y = ref.asInstanceOf[WeakReference[A]].get
   136         if (y == null) None
   137         else Some(y)
   138       }
   139     }
   140     private def store[A](x: A): A =
   141     {
   142       table.put(x, new WeakReference[Any](x))
   143       x
   144     }
   145 
   146     private def trim_bytes(s: String): String = new String(s.toCharArray)
   147 
   148     private def _cache_string(x: String): String =
   149       lookup(x) match {
   150         case Some(y) => y
   151         case None =>
   152           val z = trim_bytes(x)
   153           if (z.length > max_string) z else store(z)
   154       }
   155     private def _cache_props(x: Properties.T): Properties.T =
   156       if (x.isEmpty) x
   157       else
   158         lookup(x) match {
   159           case Some(y) => y
   160           case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
   161         }
   162     private def _cache_markup(x: Markup): Markup =
   163       lookup(x) match {
   164         case Some(y) => y
   165         case None =>
   166           x match {
   167             case Markup(name, props) =>
   168               store(Markup(_cache_string(name), _cache_props(props)))
   169           }
   170       }
   171     private def _cache_tree(x: XML.Tree): XML.Tree =
   172       lookup(x) match {
   173         case Some(y) => y
   174         case None =>
   175           x match {
   176             case XML.Elem(markup, body) =>
   177               store(XML.Elem(_cache_markup(markup), _cache_body(body)))
   178             case XML.Text(text) => store(XML.Text(_cache_string(text)))
   179           }
   180       }
   181     private def _cache_body(x: XML.Body): XML.Body =
   182       if (x.isEmpty) x
   183       else
   184         lookup(x) match {
   185           case Some(y) => y
   186           case None => x.map(_cache_tree(_))
   187         }
   188 
   189     // main methods
   190     def cache_string(x: String): String = synchronized { _cache_string(x) }
   191     def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
   192     def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
   193     def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
   194     def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
   195   }
   196 
   197 
   198 
   199   /** XML as data representation language **/
   200 
   201   class XML_Atom(s: String) extends Exception(s)
   202   class XML_Body(body: XML.Body) extends Exception
   203 
   204   object Encode
   205   {
   206     type T[A] = A => XML.Body
   207 
   208 
   209     /* atomic values */
   210 
   211     def long_atom(i: Long): String = i.toString
   212 
   213     def int_atom(i: Int): String = i.toString
   214 
   215     def bool_atom(b: Boolean): String = if (b) "1" else "0"
   216 
   217     def unit_atom(u: Unit) = ""
   218 
   219 
   220     /* structural nodes */
   221 
   222     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
   223 
   224     private def vector(xs: List[String]): XML.Attributes =
   225       xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) })
   226 
   227     private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
   228       XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
   229 
   230 
   231     /* representation of standard types */
   232 
   233     val properties: T[Properties.T] =
   234       (props => List(XML.Elem(Markup(":", props), Nil)))
   235 
   236     val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
   237 
   238     val long: T[Long] = (x => string(long_atom(x)))
   239 
   240     val int: T[Int] = (x => string(int_atom(x)))
   241 
   242     val bool: T[Boolean] = (x => string(bool_atom(x)))
   243 
   244     val unit: T[Unit] = (x => string(unit_atom(x)))
   245 
   246     def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   247       (x => List(node(f(x._1)), node(g(x._2))))
   248 
   249     def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   250       (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
   251 
   252     def list[A](f: T[A]): T[List[A]] =
   253       (xs => xs.map((x: A) => node(f(x))))
   254 
   255     def option[A](f: T[A]): T[Option[A]] =
   256     {
   257       case None => Nil
   258       case Some(x) => List(node(f(x)))
   259     }
   260 
   261     def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
   262     {
   263       case x =>
   264         val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
   265         List(tagged(tag, f(x)))
   266     }
   267   }
   268 
   269   object Decode
   270   {
   271     type T[A] = XML.Body => A
   272     type V[A] = (List[String], XML.Body) => A
   273 
   274 
   275     /* atomic values */
   276 
   277     def long_atom(s: String): Long =
   278       try { java.lang.Long.parseLong(s) }
   279       catch { case e: NumberFormatException => throw new XML_Atom(s) }
   280 
   281     def int_atom(s: String): Int =
   282       try { Integer.parseInt(s) }
   283       catch { case e: NumberFormatException => throw new XML_Atom(s) }
   284 
   285     def bool_atom(s: String): Boolean =
   286       if (s == "1") true
   287       else if (s == "0") false
   288       else throw new XML_Atom(s)
   289 
   290     def unit_atom(s: String): Unit =
   291       if (s == "") () else throw new XML_Atom(s)
   292 
   293 
   294     /* structural nodes */
   295 
   296     private def node(t: XML.Tree): XML.Body =
   297       t match {
   298         case XML.Elem(Markup(":", Nil), ts) => ts
   299         case _ => throw new XML_Body(List(t))
   300       }
   301 
   302     private def vector(atts: XML.Attributes): List[String] =
   303       atts.iterator.zipWithIndex.map(
   304         { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList
   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 }