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