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

Detecting and recoding Isabelle symbols.
*/

package isabelle

import scala.io.Source
import scala.collection.mutable
import scala.util.matching.Regex


object Symbol
{
  type Symbol = String


  /* spaces */

  val spc = ' '
  val space = " "

  private val static_spaces = space * 4000

  def spaces(k: Int): String =
  {
    require(k >= 0)
    if (k < static_spaces.length) static_spaces.substring(0, k)
    else space * k
  }


  /* ASCII characters */

  def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
  def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
  def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''

  def is_ascii_letdig(c: Char): Boolean =
    is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)

  def is_ascii_identifier(s: String): Boolean =
    s.length > 0 && is_ascii_letter(s(0)) && s.substring(1).forall(is_ascii_letdig)


  /* Symbol regexps */

  private val plain = new Regex("""(?xs)
      [^\r\\\ud800-\udfff\ufffd] | [\ud800-\udbff][\udc00-\udfff] """)

  private val physical_newline = new Regex("""(?xs) \n | \r\n | \r """)

  private val symbol = new Regex("""(?xs)
      \\ < (?:
      \^? [A-Za-z][A-Za-z0-9_']* |
      \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")

  private val malformed_symbol = new Regex("(?xs) (?!" + symbol + ")" +
    """ [\ud800-\udbff\ufffd] | \\<\^? """)

  val regex_total =
    new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + malformed_symbol + "| .")


  /* basic matching */

  def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')

  def is_physical_newline(s: Symbol): Boolean =
    s == "\n" || s == "\r" || s == "\r\n"

  def is_malformed(s: Symbol): Boolean =
    !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches

  class Matcher(text: CharSequence)
  {
    private val matcher = regex_total.pattern.matcher(text)
    def apply(start: Int, end: Int): Int =
    {
      require(0 <= start && start < end && end <= text.length)
      if (is_plain(text.charAt(start))) 1
      else {
        matcher.region(start, end).lookingAt
        matcher.group.length
      }
    }
  }


  /* iterator */

  private val char_symbols: Array[Symbol] =
    (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray

  def iterator(text: CharSequence): Iterator[Symbol] =
    new Iterator[Symbol]
    {
      private val matcher = new Matcher(text)
      private var i = 0
      def hasNext = i < text.length
      def next =
      {
        val n = matcher(i, text.length)
        val s =
          if (n == 0) ""
          else if (n == 1) {
            val c = text.charAt(i)
            if (c < char_symbols.length) char_symbols(c)
            else text.subSequence(i, i + n).toString
          }
          else text.subSequence(i, i + n).toString
        i += n
        s
      }
    }


  /* decoding offsets */

  class Index(text: CharSequence)
  {
    sealed case class Entry(chr: Int, sym: Int)
    val index: Array[Entry] =
    {
      val matcher = new Matcher(text)
      val buf = new mutable.ArrayBuffer[Entry]
      var chr = 0
      var sym = 0
      while (chr < text.length) {
        val n = matcher(chr, text.length)
        chr += n
        sym += 1
        if (n > 1) buf += Entry(chr, sym)
      }
      buf.toArray
    }
    def decode(sym1: Int): Int =
    {
      val sym = sym1 - 1
      val end = index.length
      def bisect(a: Int, b: Int): Int =
      {
        if (a < b) {
          val c = (a + b) / 2
          if (sym < index(c).sym) bisect(a, c)
          else if (c + 1 == end || sym < index(c + 1).sym) c
          else bisect(c + 1, b)<commit_msg>Symbol.explode as in ML;<commit_after>/*  Title:      Pure/General/symbol.scala
    Author:     Makarius

Detecting and recoding Isabelle symbols.
*/

package isabelle

import scala.io.Source
import scala.collection.mutable
import scala.util.matching.Regex


object Symbol
{
  type Symbol = String


  /* spaces */

  val spc = ' '
  val space = " "

  private val static_spaces = space * 4000

  def spaces(k: Int): String =
  {
    require(k >= 0)
    if (k < static_spaces.length) static_spaces.substring(0, k)
    else space * k
  }


  /* ASCII characters */

  def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
  def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
  def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''

  def is_ascii_letdig(c: Char): Boolean =
    is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)

  def is_ascii_identifier(s: String): Boolean =
    s.length > 0 && is_ascii_letter(s(0)) && s.substring(1).forall(is_ascii_letdig)


  /* Symbol regexps */

  private val plain = new Regex("""(?xs)
      [^\r\\\ud800-\udfff\ufffd] | [\ud800-\udbff][\udc00-\udfff] """)

  private val physical_newline = new Regex("""(?xs) \n | \r\n | \r """)

  private val symbol = new Regex("""(?xs)
      \\ < (?:
      \^? [A-Za-z][A-Za-z0-9_']* |
      \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")

  private val malformed_symbol = new Regex("(?xs) (?!" + symbol + ")" +
    """ [\ud800-\udbff\ufffd] | \\<\^? """)

  val regex_total =
    new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + malformed_symbol + "| .")


  /* basic matching */

  def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')

  def is_physical_newline(s: Symbol): Boolean =
    s == "\n" || s == "\r" || s == "\r\n"

  def is_malformed(s: Symbol): Boolean =
    !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches

  class Matcher(text: CharSequence)
  {
    private val matcher = regex_total.pattern.matcher(text)
    def apply(start: Int, end: Int): Int =
    {
      require(0 <= start && start < end && end <= text.length)
      if (is_plain(text.charAt(start))) 1
      else {
        matcher.region(start, end).lookingAt
        matcher.group.length
      }
    }
  }


  /* iterator */

  private val char_symbols: Array[Symbol] =
    (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray

  def iterator(text: CharSequence): Iterator[Symbol] =
    new Iterator[Symbol]
    {
      private val matcher = new Matcher(text)
      private var i = 0
      def hasNext = i < text.length
      def next =
      {
        val n = matcher(i, text.length)
        val s =
          if (n == 0) ""
          else if (n == 1) {
            val c = text.charAt(i)
            if (c < char_symbols.length) char_symbols(c)
            else text.subSequence(i, i + n).toString
          }
          else text.subSequence(i, i + n).toString
        i += n
        s
      }
    }

  def explode(text: CharSequence): List[Symbol] = iterator(text).toList


  /* decoding offsets */

  class Index(text: CharSequence)
  {
    sealed case class Entry(chr: Int, sym: Int)
    val index: Array[Entry] =
    {
      val matcher = new Matcher(text)
      val buf = new mutable.ArrayBuffer[Entry]
      var chr = 0
      var sym = 0
      while (chr < text.length) {
        val n = matcher(chr, text.length)
        chr += n
        sym += 1
        if (n > 1) buf += Entry(chr, sym)
      }
      buf.toArray
    }
    def decode(sym1: Int): Int =
    {
      val sym = sym1 - 1
      val end = index.length
      def bisect(a: Int, b: Int): Int =
      {
        if (a < b) {
          val c = (a + b) / 2
          if (sym < index(c).sym) bisect(a, c)
          else if (c + 1 == end || sym < index(c + 1).sym) c
          else bisect(c + 1, b)
{'fraction_non_alphanumeric': 0.16957541026308934, 'fraction_numerical': 0.014587132065642095, 'mean_word_length': 2.1876297218762972, 'pattern_counts': {'":': 0, '<': 43, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, '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': '98245', 'n_tokens_mistral': 2928, 'n_tokens_neox': 2732, 'n_words': 683}