src/Pure/PIDE/yxml.scala
author wenzelm
Sun Sep 04 15:21:50 2011 +0200 (2011-09-04 ago)
changeset 44698 0385292321a0
parent 44181 src/Pure/General/yxml.scala@bbce0417236d
child 45666 d83797ef0d2d
permissions -rw-r--r--
moved XML/YXML to src/Pure/PIDE;
tuned comments;
     1 /*  Title:      Pure/PIDE/yxml.scala
     2     Author:     Makarius
     3 
     4 Efficient text representation of XML trees.  Suitable for direct
     5 inlining into plain text.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.collection.mutable
    12 
    13 
    14 object YXML
    15 {
    16   /* chunk markers */
    17 
    18   val X = '\5'
    19   val Y = '\6'
    20   val X_string = X.toString
    21   val Y_string = Y.toString
    22 
    23   def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
    24 
    25 
    26   /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
    27 
    28   def string_of_body(body: XML.Body): String =
    29   {
    30     val s = new StringBuilder
    31     def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
    32     def tree(t: XML.Tree): Unit =
    33       t match {
    34         case XML.Elem(Markup(name, atts), ts) =>
    35           s += X; s += Y; s++= name; atts.foreach(attrib); s += X
    36           ts.foreach(tree)
    37           s += X; s += Y; s += X
    38         case XML.Text(text) => s ++= text
    39       }
    40     body.foreach(tree)
    41     s.toString
    42   }
    43 
    44   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
    45 
    46 
    47   /* parsing */
    48 
    49   private def err(msg: String) = error("Malformed YXML: " + msg)
    50   private def err_attribute() = err("bad attribute")
    51   private def err_element() = err("bad element")
    52   private def err_unbalanced(name: String) =
    53     if (name == "") err("unbalanced element")
    54     else err("unbalanced element " + quote(name))
    55 
    56   private def parse_attrib(source: CharSequence) = {
    57     val s = source.toString
    58     val i = s.indexOf('=')
    59     if (i <= 0) err_attribute()
    60     (s.substring(0, i), s.substring(i + 1))
    61   }
    62 
    63 
    64   def parse_body(source: CharSequence): XML.Body =
    65   {
    66     /* stack operations */
    67 
    68     def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
    69     var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
    70 
    71     def add(x: XML.Tree)
    72     {
    73       (stack: @unchecked) match { case ((_, body) :: _) => body += x }
    74     }
    75 
    76     def push(name: String, atts: XML.Attributes)
    77     {
    78       if (name == "") err_element()
    79       else stack = (Markup(name, atts), buffer()) :: stack
    80     }
    81 
    82     def pop()
    83     {
    84       (stack: @unchecked) match {
    85         case ((Markup.Empty, _) :: _) => err_unbalanced("")
    86         case ((markup, body) :: pending) =>
    87           stack = pending
    88           add(XML.Elem(markup, body.toList))
    89       }
    90     }
    91 
    92 
    93     /* parse chunks */
    94 
    95     for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
    96       if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
    97       else {
    98         Library.chunks(chunk, Y).toList match {
    99           case ch :: name :: atts if ch.length == 0 =>
   100             push(name.toString, atts.map(parse_attrib))
   101           case txts => for (txt <- txts) add(XML.Text(txt.toString))
   102         }
   103       }
   104     }
   105     (stack: @unchecked) match {
   106       case List((Markup.Empty, body)) => body.toList
   107       case (Markup(name, _), _) :: _ => err_unbalanced(name)
   108     }
   109   }
   110 
   111   def parse(source: CharSequence): XML.Tree =
   112     parse_body(source) match {
   113       case List(result) => result
   114       case Nil => XML.Text("")
   115       case _ => err("multiple results")
   116     }
   117 
   118 
   119   /* failsafe parsing */
   120 
   121   private def markup_malformed(source: CharSequence) =
   122     XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
   123 
   124   def parse_body_failsafe(source: CharSequence): XML.Body =
   125   {
   126     try { parse_body(source) }
   127     catch { case ERROR(_) => List(markup_malformed(source)) }
   128   }
   129 
   130   def parse_failsafe(source: CharSequence): XML.Tree =
   131   {
   132     try { parse(source) }
   133     catch { case ERROR(_) => markup_malformed(source) }
   134   }
   135 }