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