Quelle yxml.scala Sprache: Scala

/*  Title:      Pure/PIDE/yxml.scala
    Author:     Makarius

Efficient text representation of XML trees.  Suitable for direct
inlining into plain text.
*/

package isabelle

import scala.collection.mutable

object YXML {
  /* chunk markers */

  val X_byte: Byte = 5
  val Y_byte: Byte = 6

  val X_char: Char = X_byte.toChar
  val Y_char: Char = Y_byte.toChar

  val X_string: String = X_char.toString
  val Y_string: String = Y_char.toString

  def detect(s: String): Boolean = s.exists(c => c == X_char || c == Y_char)
  def detect_elem(s: String): Boolean = s.length >= 2 && s(0) == X_char && s(1) == Y_char

  /* string representation */

  trait Output extends XML.Traversal {
    def byte(b: Byte): Unit
    def string(s: String): Unit

    // XML.Traversal
    override def text(s: String): Unit = string(s)
    override def elem(markup: Markup, end: Boolean = false): Unit = {
      byte(X_byte)
      byte(Y_byte)
      string(markup.name)
      for ((a, b) <- markup.properties) {
        byte(Y_byte)
        string(a)
        byte('='.toByte)
        string(b)
      }
      byte(X_byte)
      if (end) end_elem(markup.name)
    }
    override def end_elem(name: String): Unit = {
      byte(X_byte)
      byte(Y_byte)
      byte(X_byte)
    }
  }

  class Output_String(builder: StringBuilder, recode: String => String = identity) extends Output {
    override def byte(b: Byte): Unit = { builder += b.toChar }
    override def string(s: String): Unit = { builder ++= recode(s) }
    def result(ts: List[XML.Tree]): String = { traverse(ts); builder.toString }
  }

  class Output_Bytes(builder: Bytes.Builder, recode: String => String = identity) extends Output {
    override def byte(b: Byte): Unit = { builder += b }
    override def string(s: String): Unit = { builder += recode(s) }
  }

  def string_of_body(body: XML.Body, recode: String => String = identity): String =
    new Output_String(new StringBuilder, recode = recode).result(body)

  def string_of_tree(tree: XML.Tree, recode: String => String = identity): String =
    string_of_body(List(tree), recode = recode)

  def bytes_of_body(body: XML.Body, recode: String => String = identity): Bytes =
    Bytes.Builder.use()(builder => new Output_Bytes(builder, recode = recode).traverse(body))

  def bytes_of_tree(tree: XML.Tree, recode: String => String = identity): Bytes =
    bytes_of_body(List(tree), recode = recode)

  /* parsing */

  private def err(msg: String) = error("Malformed YXML: " + msg)
  private def err_attribute() = err("bad attribute")
  private def err_element() = err("bad element")
  private def err_unbalanced(name: String) =
    if (name == "") err("unbalanced element")
    else err("unbalanced element " + quote(name))

  object Source {
    def apply(s: String): Source = new Source_String(s)
  }

  trait Source {
    def is_empty: Boolean
    def is_X: Boolean
    def is_Y: Boolean
    def iterator_X: Iterator[Source]
    def iterator_Y: Iterator[Source]
    def text: String
  }

  class Source_String(source: String) extends Source {
    override def is_empty: Boolean = source.isEmpty
    override def is_X: Boolean = source.length == 1 && source(0) == X_char
    override def is_Y: Boolean = source.length == 1 && source(0) == Y_char
    override def iterator_X: Iterator[Source] =
      Library.separated_chunks(X_char, source).map(Source.apply)
    override def iterator_Y: Iterator[Source] =
      Library.separated_chunks(Y_char, source).map(Source.apply)
    override def text: String = source
  }

  def parse_body(
    source: Source,
    recode: String => String = identity,
    cache: XML.Cache = XML.Cache.none
  ): XML.Body = {
    /* parse + recode */

    def parse_string(s: Source): String = recode(s.text)

    def parse_attrib(s: Source): (String, String) =
      Properties.Eq.unapply(parse_string(s)) getOrElse err_attribute()

    /* stack operations */

    def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
    var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))

    def add(x: XML.Tree): Unit =
      (stack: @unchecked) match { case (_, body) :: _ => body += x }

    def push(name: String, atts: XML.Attributes): Unit =
      if (name == "") err_element()
      else stack = (cache.markup(Markup(name, atts)), buffer()) :: stack

    def pop(): Unit =
      (stack: @unchecked) match {
        case (Markup.Empty, _) :: _ => err_unbalanced("")
        case (markup, body) :: pending =>
          stack = pending
          add(cache.tree0(XML.Elem(markup, body.toList)))
      }

    /* parse chunks */

    for (chunk <- source.iterator_X) {
      if (!chunk.is_empty) {
        if (chunk.is_Y) pop()
        else {
          chunk.iterator_Y.toList match {
            case ch :: name :: atts if ch.is_empty =>
              push(parse_string(name), atts.map(parse_attrib))
            case txts =>
              for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt)))))
          }
        }
      }
    }
    (stack: @unchecked) match {
      case List((Markup.Empty, body)) => body.toList
      case (Markup(name, _), _) :: _ => err_unbalanced(name)
    }
  }

  def parse(
    source: Source,
    recode: String => String = identity,
    cache: XML.Cache = XML.Cache.none
  ): XML.Tree =
    parse_body(source, recode = recode, cache = cache) match {
      case List(result) => result
      case Nil => XML.no_text
      case _ => err("multiple XML trees")
    }

  def parse_elem(
    source: Source,
    recode: String => String = identity,
    cache: XML.Cache = XML.Cache.none
  ): XML.Tree =
    parse_body(source, recode = recode, cache = cache) match {
      case List(elem: XML.Elem) => elem
      case _ => err("single XML element expected")
    }

  /* failsafe parsing */

  private def markup_broken(source: Source) =
    XML.Elem(Markup.Broken, List(XML.Text(source.toString)))

  def parse_body_failsafe(
    source: Source,
    recode: String => String = identity,
    cache: XML.Cache = XML.Cache.none
  ): XML.Body = {
    try { parse_body(source, recode = recode, cache = cache) }
    catch { case ERROR(_) => List(markup_broken(source)) }
  }

  def parse_failsafe(
    source: Source,
    recode: String => String = identity,
    cache: XML.Cache = XML.Cache.none
  ): XML.Tree = {
    try { parse(source, recode = recode, cache = cache) }
    catch { case ERROR(_) => markup_broken(source) }
  }
}

quality91%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.