/*  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'

 }