<commit_before>/*  Title:      Pure/General/yxml.scala
    Author:     Makarius

Efficient text representation of XML trees.
*/

package isabelle


import scala.collection.mutable.ListBuffer


object YXML
{
  /* chunk markers */

  private val X = '\5'
  private val Y = '\6'
  private val X_string = X.toString
  private val Y_string = Y.toString


  /* decoding pseudo UTF-8 */

  private class Decode_Chars(decode: String => String,
    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
  {
    def length: Int = end - start
    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
    def subSequence(i: Int, j: Int): CharSequence =
      new Decode_Chars(decode, buffer, start + i, start + j)

    // toString with adhoc decoding: abuse of CharSequence interface
    override def toString: String = decode(Standard_System.decode_permissive_utf8(this))
  }

  def decode_chars(decode: String => String,
    buffer: Array[Byte], start: Int, end: Int): CharSequence =
  {
    require(0 <= start && start <= end && end <= buffer.length)
    new Decode_Chars(decode, buffer, start, end)
  }


  /* 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 \"" + name + "\"")

  private def parse_attrib(source: CharSequence) = {
    val s = source.toString
    val i = s.indexOf('=')
    if (i <= 0) err_attribute()
    (s.substring(0, i).intern, s.substring(i + 1))
  }


  def parse_body(source: CharSequence): List[XML.Tree] =
  {
    /* stack operations */

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

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

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

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


    /* parse chunks */

    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
      if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
      else {
        Library.chunks(chunk, Y).toList match {
          case ch :: name :: atts if ch.length == 0 =>
            push(name.toString.intern, atts.map(parse_attrib))
          case txts => for (txt <- txts) add(XML.Text(txt.toString))
        }
      }
    }
    stack match {
      case List((Markup("", _), body)) => body.toList
      case (Markup(name, _), _) :: _ => err_unbalanced(name)
    }<commit_msg>YXML.parse: refrain from interning, let XML.Cache do it (partially);<commit_after>/*  Title:      Pure/General/yxml.scala
    Author:     Makarius

Efficient text representation of XML trees.
*/

package isabelle


import scala.collection.mutable.ListBuffer


object YXML
{
  /* chunk markers */

  private val X = '\5'
  private val Y = '\6'
  private val X_string = X.toString
  private val Y_string = Y.toString


  /* decoding pseudo UTF-8 */

  private class Decode_Chars(decode: String => String,
    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
  {
    def length: Int = end - start
    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
    def subSequence(i: Int, j: Int): CharSequence =
      new Decode_Chars(decode, buffer, start + i, start + j)

    // toString with adhoc decoding: abuse of CharSequence interface
    override def toString: String = decode(Standard_System.decode_permissive_utf8(this))
  }

  def decode_chars(decode: String => String,
    buffer: Array[Byte], start: Int, end: Int): CharSequence =
  {
    require(0 <= start && start <= end && end <= buffer.length)
    new Decode_Chars(decode, buffer, start, end)
  }


  /* 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 \"" + name + "\"")

  private def parse_attrib(source: CharSequence) = {
    val s = source.toString
    val i = s.indexOf('=')
    if (i <= 0) err_attribute()
    (s.substring(0, i), s.substring(i + 1))
  }


  def parse_body(source: CharSequence): List[XML.Tree] =
  {
    /* stack operations */

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

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

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

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


    /* parse chunks */

    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
      if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
      else {
        Library.chunks(chunk, Y).toList match {
          case ch :: name :: atts if ch.length == 0 =>
            push(name.toString, atts.map(parse_attrib))
          case txts => for (txt <- txts) add(XML.Text(txt.toString))
        }
      }
    }
    stack match {
      case List((Markup("", _), body)) => body.toList
      case (Markup(name, _), _) :: _ => err_unbalanced(name)
    }
{'fraction_non_alphanumeric': 0.15151515151515152, 'fraction_numerical': 0.00430534856764365, 'mean_word_length': 2.7868338557993733, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 2}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2332503', 'n_tokens_mistral': 2031, 'n_tokens_neox': 1942, 'n_words': 528}