/*  THIS IS A PARTIAL COPY OF Isabelle2016-1 ...

    Title:      Pure/General/symbol.scala

    Author:     Makarius

    ... WITH ADDITIONS AFTER "/---..---\"

Detecting and recoding Isabelle symbols.

*/

package isac.gui.mawen.syntax.isabelle

import scala.collection.mutable

import scala.util.matching.Regex

import scala.annotation.tailrec

object XSymbol

{

  type Symbol = String

  // counting Isabelle symbols, starting from 1

  type Offset = Text.Offset

  type Range = Text.Range

  /* spaces */

  val space = " "

  private val static_spaces = space * 4000

  def spaces(n: Int): String =

  {

    require(n >= 0)

    if (n < static_spaces.length) static_spaces.substring(0, n)

    else space * n

  }

  /* 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_hex(c: Char): Boolean =

    '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'

  def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''

  def is_ascii_blank(c: Char): Boolean = " \t\n\u000b\f\r".contains(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.forall(is_ascii_letdig)

  def ascii(c: Char): Symbol =

  {

    if (c > 127) error("Non-ASCII character: " + XLibrary.quote(c.toString))

    else char_symbols(c.toInt)

  }

  /* symbol matching */

  private val symbol_total = new Regex("""(?xs)

    [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""")

  private def is_plain(c: Char): Boolean =

    !(c == '\r' || c == '\\' || Character.isHighSurrogate(c))

  def is_malformed(s: Symbol): Boolean =

    s.length match {

      case 1 =>

        val c = s(0)

        Character.isHighSurrogate(c) || Character.isLowSurrogate(c) || c == '\ufffd'

      case 2 =>

        val c1 = s(0)

        val c2 = s(1)

        !(c1 == '\r' && c2 == '\n' || Character.isSurrogatePair(c1, c2))

      case _ => !s.endsWith(">") || s == "\\<>" || s == "\\<^>"

    }

  def is_newline(s: Symbol): Boolean =

    s == "\n" || s == "\r" || s == "\r\n"

  class Matcher(text: CharSequence)

  {

    private val matcher = symbol_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

  def advance_line_column(pos: (Int, Int), text: CharSequence): (Int, Int) =

  {

    var (line, column) = pos

    for (sym <- iterator(text)) {

      if (is_newline(sym)) { line += 1; column = 1 }

      else column += 1

    }

    (line, column)

  }

  /* decoding offsets */

  object Index

  {

    private sealed case class Entry(chr: Int, sym: Int)

    val empty: Index = new Index(Nil)

    def apply(text: CharSequence): Index =

    {

      val matcher = new Matcher(text)

      val buf = new mutable.ListBuffer[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)

      }

      if (buf.isEmpty) empty else new Index(buf.toList)

    }

  }

  final class Index private(entries: List[Index.Entry])

  {

    private val hash: Int = entries.hashCode

    private val index: Array[Index.Entry] = entries.toArray

    def decode(symbol_offset: Offset): Text.Offset =

    {

      val sym = symbol_offset - 1

      val end = index.length

      @tailrec 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)

        }

        else -1

      }

      val i = bisect(0, end)

      if (i < 0) sym

      else index(i).chr + sym - index(i).sym

    }

    def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))

    override def hashCode: Int = hash

    override def equals(that: Any): Boolean =

      that match {

        case other: Index => index.sameElements(other.index)

        case _ => false

      }

  }

//\\----------------- FROM HERE ON TOO ADVANCED ----------------------------//

////----------------- ADDITIONS TO Isabelle2016-1 FOR ISAC -----------------\\

  //                Symbol

  def is_digit(sym: Char): Boolean = '0' <= sym && sym <= '9'

}