src/Pure/PIDE/yxml.scala
changeset 44698 0385292321a0
parent 44181 bbce0417236d
child 45666 d83797ef0d2d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/yxml.scala	Sun Sep 04 15:21:50 2011 +0200
     1.3 @@ -0,0 +1,135 @@
     1.4 +/*  Title:      Pure/PIDE/yxml.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Efficient text representation of XML trees.  Suitable for direct
     1.8 +inlining into plain text.
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +import scala.collection.mutable
    1.15 +
    1.16 +
    1.17 +object YXML
    1.18 +{
    1.19 +  /* chunk markers */
    1.20 +
    1.21 +  val X = '\5'
    1.22 +  val Y = '\6'
    1.23 +  val X_string = X.toString
    1.24 +  val Y_string = Y.toString
    1.25 +
    1.26 +  def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
    1.27 +
    1.28 +
    1.29 +  /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
    1.30 +
    1.31 +  def string_of_body(body: XML.Body): String =
    1.32 +  {
    1.33 +    val s = new StringBuilder
    1.34 +    def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
    1.35 +    def tree(t: XML.Tree): Unit =
    1.36 +      t match {
    1.37 +        case XML.Elem(Markup(name, atts), ts) =>
    1.38 +          s += X; s += Y; s++= name; atts.foreach(attrib); s += X
    1.39 +          ts.foreach(tree)
    1.40 +          s += X; s += Y; s += X
    1.41 +        case XML.Text(text) => s ++= text
    1.42 +      }
    1.43 +    body.foreach(tree)
    1.44 +    s.toString
    1.45 +  }
    1.46 +
    1.47 +  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
    1.48 +
    1.49 +
    1.50 +  /* parsing */
    1.51 +
    1.52 +  private def err(msg: String) = error("Malformed YXML: " + msg)
    1.53 +  private def err_attribute() = err("bad attribute")
    1.54 +  private def err_element() = err("bad element")
    1.55 +  private def err_unbalanced(name: String) =
    1.56 +    if (name == "") err("unbalanced element")
    1.57 +    else err("unbalanced element " + quote(name))
    1.58 +
    1.59 +  private def parse_attrib(source: CharSequence) = {
    1.60 +    val s = source.toString
    1.61 +    val i = s.indexOf('=')
    1.62 +    if (i <= 0) err_attribute()
    1.63 +    (s.substring(0, i), s.substring(i + 1))
    1.64 +  }
    1.65 +
    1.66 +
    1.67 +  def parse_body(source: CharSequence): XML.Body =
    1.68 +  {
    1.69 +    /* stack operations */
    1.70 +
    1.71 +    def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
    1.72 +    var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
    1.73 +
    1.74 +    def add(x: XML.Tree)
    1.75 +    {
    1.76 +      (stack: @unchecked) match { case ((_, body) :: _) => body += x }
    1.77 +    }
    1.78 +
    1.79 +    def push(name: String, atts: XML.Attributes)
    1.80 +    {
    1.81 +      if (name == "") err_element()
    1.82 +      else stack = (Markup(name, atts), buffer()) :: stack
    1.83 +    }
    1.84 +
    1.85 +    def pop()
    1.86 +    {
    1.87 +      (stack: @unchecked) match {
    1.88 +        case ((Markup.Empty, _) :: _) => err_unbalanced("")
    1.89 +        case ((markup, body) :: pending) =>
    1.90 +          stack = pending
    1.91 +          add(XML.Elem(markup, body.toList))
    1.92 +      }
    1.93 +    }
    1.94 +
    1.95 +
    1.96 +    /* parse chunks */
    1.97 +
    1.98 +    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
    1.99 +      if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
   1.100 +      else {
   1.101 +        Library.chunks(chunk, Y).toList match {
   1.102 +          case ch :: name :: atts if ch.length == 0 =>
   1.103 +            push(name.toString, atts.map(parse_attrib))
   1.104 +          case txts => for (txt <- txts) add(XML.Text(txt.toString))
   1.105 +        }
   1.106 +      }
   1.107 +    }
   1.108 +    (stack: @unchecked) match {
   1.109 +      case List((Markup.Empty, body)) => body.toList
   1.110 +      case (Markup(name, _), _) :: _ => err_unbalanced(name)
   1.111 +    }
   1.112 +  }
   1.113 +
   1.114 +  def parse(source: CharSequence): XML.Tree =
   1.115 +    parse_body(source) match {
   1.116 +      case List(result) => result
   1.117 +      case Nil => XML.Text("")
   1.118 +      case _ => err("multiple results")
   1.119 +    }
   1.120 +
   1.121 +
   1.122 +  /* failsafe parsing */
   1.123 +
   1.124 +  private def markup_malformed(source: CharSequence) =
   1.125 +    XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
   1.126 +
   1.127 +  def parse_body_failsafe(source: CharSequence): XML.Body =
   1.128 +  {
   1.129 +    try { parse_body(source) }
   1.130 +    catch { case ERROR(_) => List(markup_malformed(source)) }
   1.131 +  }
   1.132 +
   1.133 +  def parse_failsafe(source: CharSequence): XML.Tree =
   1.134 +  {
   1.135 +    try { parse(source) }
   1.136 +    catch { case ERROR(_) => markup_malformed(source) }
   1.137 +  }
   1.138 +}