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