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