src/Pure/General/symbol.scala
author wenzelm
Sat Sep 17 16:19:40 2011 +0200 (2011-09-17)
changeset 44949 b49d7f1066c8
parent 44238 36120feb70ed
child 44992 aa34d2d049ce
permissions -rw-r--r--
Symbol.explode as in ML;
wenzelm@27901
     1
/*  Title:      Pure/General/symbol.scala
wenzelm@27901
     2
    Author:     Makarius
wenzelm@27901
     3
wenzelm@27924
     4
Detecting and recoding Isabelle symbols.
wenzelm@27901
     5
*/
wenzelm@27901
     6
wenzelm@27901
     7
package isabelle
wenzelm@27901
     8
wenzelm@27918
     9
import scala.io.Source
wenzelm@36011
    10
import scala.collection.mutable
wenzelm@31522
    11
import scala.util.matching.Regex
wenzelm@27901
    12
wenzelm@27901
    13
wenzelm@31522
    14
object Symbol
wenzelm@31522
    15
{
wenzelm@43696
    16
  type Symbol = String
wenzelm@43696
    17
wenzelm@43696
    18
wenzelm@36763
    19
  /* spaces */
wenzelm@36763
    20
wenzelm@36816
    21
  val spc = ' '
wenzelm@36816
    22
  val space = " "
wenzelm@36816
    23
wenzelm@36816
    24
  private val static_spaces = space * 4000
wenzelm@36763
    25
wenzelm@36763
    26
  def spaces(k: Int): String =
wenzelm@36763
    27
  {
wenzelm@36763
    28
    require(k >= 0)
wenzelm@36763
    29
    if (k < static_spaces.length) static_spaces.substring(0, k)
wenzelm@36816
    30
    else space * k
wenzelm@36763
    31
  }
wenzelm@36763
    32
wenzelm@36763
    33
wenzelm@43418
    34
  /* ASCII characters */
wenzelm@43418
    35
wenzelm@43418
    36
  def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
wenzelm@43418
    37
  def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
wenzelm@43418
    38
  def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''
wenzelm@43418
    39
wenzelm@43418
    40
  def is_ascii_letdig(c: Char): Boolean =
wenzelm@43418
    41
    is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)
wenzelm@43418
    42
wenzelm@43418
    43
  def is_ascii_identifier(s: String): Boolean =
wenzelm@43418
    44
    s.length > 0 && is_ascii_letter(s(0)) && s.substring(1).forall(is_ascii_letdig)
wenzelm@43418
    45
wenzelm@43418
    46
wenzelm@33998
    47
  /* Symbol regexps */
wenzelm@27901
    48
wenzelm@31522
    49
  private val plain = new Regex("""(?xs)
wenzelm@40524
    50
      [^\r\\\ud800-\udfff\ufffd] | [\ud800-\udbff][\udc00-\udfff] """)
wenzelm@37556
    51
wenzelm@40522
    52
  private val physical_newline = new Regex("""(?xs) \n | \r\n | \r """)
wenzelm@27901
    53
wenzelm@31522
    54
  private val symbol = new Regex("""(?xs)
wenzelm@31545
    55
      \\ < (?:
wenzelm@27924
    56
      \^? [A-Za-z][A-Za-z0-9_']* |
wenzelm@27924
    57
      \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
wenzelm@27924
    58
wenzelm@40523
    59
  private val malformed_symbol = new Regex("(?xs) (?!" + symbol + ")" +
wenzelm@40529
    60
    """ [\ud800-\udbff\ufffd] | \\<\^? """)
wenzelm@27924
    61
wenzelm@40523
    62
  val regex_total =
wenzelm@40523
    63
    new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + malformed_symbol + "| .")
wenzelm@27937
    64
wenzelm@34137
    65
wenzelm@34137
    66
  /* basic matching */
wenzelm@34137
    67
wenzelm@37556
    68
  def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
wenzelm@34137
    69
wenzelm@43696
    70
  def is_physical_newline(s: Symbol): Boolean =
wenzelm@43675
    71
    s == "\n" || s == "\r" || s == "\r\n"
wenzelm@38877
    72
wenzelm@43696
    73
  def is_malformed(s: Symbol): Boolean =
wenzelm@43675
    74
    !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches
wenzelm@34137
    75
wenzelm@34137
    76
  class Matcher(text: CharSequence)
wenzelm@34137
    77
  {
wenzelm@40523
    78
    private val matcher = regex_total.pattern.matcher(text)
wenzelm@34137
    79
    def apply(start: Int, end: Int): Int =
wenzelm@34137
    80
    {
wenzelm@34137
    81
      require(0 <= start && start < end && end <= text.length)
wenzelm@34316
    82
      if (is_plain(text.charAt(start))) 1
wenzelm@34138
    83
      else {
wenzelm@34137
    84
        matcher.region(start, end).lookingAt
wenzelm@34137
    85
        matcher.group.length
wenzelm@34137
    86
      }
wenzelm@34137
    87
    }
wenzelm@31522
    88
  }
wenzelm@27937
    89
wenzelm@27937
    90
wenzelm@43695
    91
  /* iterator */
wenzelm@33998
    92
wenzelm@43696
    93
  private val char_symbols: Array[Symbol] =
wenzelm@43675
    94
    (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
wenzelm@43675
    95
wenzelm@43696
    96
  def iterator(text: CharSequence): Iterator[Symbol] =
wenzelm@43696
    97
    new Iterator[Symbol]
wenzelm@40522
    98
    {
wenzelm@43489
    99
      private val matcher = new Matcher(text)
wenzelm@43489
   100
      private var i = 0
wenzelm@43489
   101
      def hasNext = i < text.length
wenzelm@43489
   102
      def next =
wenzelm@43489
   103
      {
wenzelm@43489
   104
        val n = matcher(i, text.length)
wenzelm@43675
   105
        val s =
wenzelm@43675
   106
          if (n == 0) ""
wenzelm@43675
   107
          else if (n == 1) {
wenzelm@43675
   108
            val c = text.charAt(i)
wenzelm@43675
   109
            if (c < char_symbols.length) char_symbols(c)
wenzelm@43675
   110
            else text.subSequence(i, i + n).toString
wenzelm@43675
   111
          }
wenzelm@43675
   112
          else text.subSequence(i, i + n).toString
wenzelm@43489
   113
        i += n
wenzelm@43489
   114
        s
wenzelm@43489
   115
      }
wenzelm@33998
   116
    }
wenzelm@43489
   117
wenzelm@44949
   118
  def explode(text: CharSequence): List[Symbol] = iterator(text).toList
wenzelm@44949
   119
wenzelm@33998
   120
wenzelm@33998
   121
  /* decoding offsets */
wenzelm@33998
   122
wenzelm@33998
   123
  class Index(text: CharSequence)
wenzelm@31929
   124
  {
wenzelm@43714
   125
    sealed case class Entry(chr: Int, sym: Int)
wenzelm@31929
   126
    val index: Array[Entry] =
wenzelm@31929
   127
    {
wenzelm@34137
   128
      val matcher = new Matcher(text)
wenzelm@31929
   129
      val buf = new mutable.ArrayBuffer[Entry]
wenzelm@31929
   130
      var chr = 0
wenzelm@31929
   131
      var sym = 0
wenzelm@33998
   132
      while (chr < text.length) {
wenzelm@34137
   133
        val n = matcher(chr, text.length)
wenzelm@34137
   134
        chr += n
wenzelm@31929
   135
        sym += 1
wenzelm@34137
   136
        if (n > 1) buf += Entry(chr, sym)
wenzelm@31929
   137
      }
wenzelm@31929
   138
      buf.toArray
wenzelm@31929
   139
    }
wenzelm@38479
   140
    def decode(sym1: Int): Int =
wenzelm@31929
   141
    {
wenzelm@38479
   142
      val sym = sym1 - 1
wenzelm@31929
   143
      val end = index.length
wenzelm@31929
   144
      def bisect(a: Int, b: Int): Int =
wenzelm@31929
   145
      {
wenzelm@31929
   146
        if (a < b) {
wenzelm@31929
   147
          val c = (a + b) / 2
wenzelm@31929
   148
          if (sym < index(c).sym) bisect(a, c)
wenzelm@31929
   149
          else if (c + 1 == end || sym < index(c + 1).sym) c
wenzelm@31929
   150
          else bisect(c + 1, b)
wenzelm@31929
   151
        }
wenzelm@31929
   152
        else -1
wenzelm@31929
   153
      }
wenzelm@31929
   154
      val i = bisect(0, end)
wenzelm@31929
   155
      if (i < 0) sym
wenzelm@31929
   156
      else index(i).chr + sym - index(i).sym
wenzelm@31929
   157
    }
wenzelm@38479
   158
    def decode(range: Text.Range): Text.Range = range.map(decode(_))
wenzelm@31929
   159
  }
wenzelm@31929
   160
wenzelm@31929
   161
wenzelm@33998
   162
  /* recoding text */
wenzelm@27937
   163
wenzelm@31522
   164
  private class Recoder(list: List[(String, String)])
wenzelm@31522
   165
  {
wenzelm@31522
   166
    private val (min, max) =
wenzelm@31522
   167
    {
wenzelm@27937
   168
      var min = '\uffff'
wenzelm@27937
   169
      var max = '\u0000'
wenzelm@27937
   170
      for ((x, _) <- list) {
wenzelm@27937
   171
        val c = x(0)
wenzelm@27937
   172
        if (c < min) min = c
wenzelm@27937
   173
        if (c > max) max = c
wenzelm@27937
   174
      }
wenzelm@27937
   175
      (min, max)
wenzelm@27937
   176
    }
wenzelm@40443
   177
    private val table =
wenzelm@40443
   178
    {
wenzelm@40443
   179
      var tab = Map[String, String]()
wenzelm@40443
   180
      for ((x, y) <- list) {
wenzelm@40443
   181
        tab.get(x) match {
wenzelm@40443
   182
          case None => tab += (x -> y)
wenzelm@40443
   183
          case Some(z) =>
wenzelm@44181
   184
            error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
wenzelm@40443
   185
        }
wenzelm@40443
   186
      }
wenzelm@40443
   187
      tab
wenzelm@40443
   188
    }
wenzelm@31522
   189
    def recode(text: String): String =
wenzelm@31522
   190
    {
wenzelm@27937
   191
      val len = text.length
wenzelm@40523
   192
      val matcher = regex_total.pattern.matcher(text)
wenzelm@27937
   193
      val result = new StringBuilder(len)
wenzelm@27937
   194
      var i = 0
wenzelm@27937
   195
      while (i < len) {
wenzelm@27937
   196
        val c = text(i)
wenzelm@27937
   197
        if (min <= c && c <= max) {
wenzelm@31929
   198
          matcher.region(i, len).lookingAt
wenzelm@27938
   199
          val x = matcher.group
wenzelm@31522
   200
          result.append(table.get(x) getOrElse x)
wenzelm@27937
   201
          i = matcher.end
wenzelm@27937
   202
        }
wenzelm@27937
   203
        else { result.append(c); i += 1 }
wenzelm@27937
   204
      }
wenzelm@27937
   205
      result.toString
wenzelm@27937
   206
    }
wenzelm@27937
   207
  }
wenzelm@27924
   208
wenzelm@27918
   209
wenzelm@27923
   210
wenzelm@43695
   211
  /** symbol interpretation **/
wenzelm@27927
   212
wenzelm@43695
   213
  private lazy val symbols =
wenzelm@43695
   214
    new Interpretation(
wenzelm@43695
   215
      Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS"))))
wenzelm@43695
   216
wenzelm@43695
   217
  private class Interpretation(symbols_spec: String)
wenzelm@29569
   218
  {
wenzelm@31522
   219
    /* read symbols */
wenzelm@31522
   220
wenzelm@31522
   221
    private val empty = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
wenzelm@31522
   222
    private val key = new Regex("""(?xs) (.+): """)
wenzelm@31522
   223
wenzelm@43696
   224
    private def read_decl(decl: String): (Symbol, Map[String, String]) =
wenzelm@31522
   225
    {
wenzelm@31522
   226
      def err() = error("Bad symbol declaration: " + decl)
wenzelm@31522
   227
wenzelm@31522
   228
      def read_props(props: List[String]): Map[String, String] =
wenzelm@31522
   229
      {
wenzelm@31522
   230
        props match {
wenzelm@31522
   231
          case Nil => Map()
wenzelm@31522
   232
          case _ :: Nil => err()
wenzelm@31522
   233
          case key(x) :: y :: rest => read_props(rest) + (x -> y)
wenzelm@31522
   234
          case _ => err()
wenzelm@31522
   235
        }
wenzelm@31522
   236
      }
wenzelm@31522
   237
      decl.split("\\s+").toList match {
wenzelm@40523
   238
        case sym :: props if sym.length > 1 && !is_malformed(sym) => (sym, read_props(props))
wenzelm@34193
   239
        case _ => err()
wenzelm@31522
   240
      }
wenzelm@31522
   241
    }
wenzelm@31522
   242
wenzelm@43696
   243
    private val symbols: List[(Symbol, Map[String, String])] =
wenzelm@40443
   244
      Map((
wenzelm@43695
   245
        for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
wenzelm@40443
   246
          yield read_decl(decl)): _*) toList
wenzelm@31522
   247
wenzelm@31522
   248
wenzelm@31651
   249
    /* misc properties */
wenzelm@31651
   250
wenzelm@43696
   251
    val names: Map[Symbol, String] =
wenzelm@34134
   252
    {
wenzelm@43456
   253
      val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
wenzelm@31651
   254
      Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
wenzelm@31651
   255
    }
wenzelm@31651
   256
wenzelm@43696
   257
    val abbrevs: Map[Symbol, String] =
wenzelm@43488
   258
      Map((
wenzelm@43488
   259
        for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
wenzelm@43488
   260
          yield (sym -> props("abbrev"))): _*)
wenzelm@43488
   261
wenzelm@43488
   262
wenzelm@43490
   263
    /* recoding */
wenzelm@31522
   264
wenzelm@31522
   265
    private val (decoder, encoder) =
wenzelm@31522
   266
    {
wenzelm@31522
   267
      val mapping =
wenzelm@31522
   268
        for {
wenzelm@31522
   269
          (sym, props) <- symbols
wenzelm@31522
   270
          val code =
wenzelm@31522
   271
            try { Integer.decode(props("code")).intValue }
wenzelm@31522
   272
            catch {
wenzelm@31522
   273
              case _: NoSuchElementException => error("Missing code for symbol " + sym)
wenzelm@31522
   274
              case _: NumberFormatException => error("Bad code for symbol " + sym)
wenzelm@31522
   275
            }
wenzelm@31522
   276
          val ch = new String(Character.toChars(code))
wenzelm@34193
   277
        } yield {
wenzelm@34193
   278
          if (code < 128) error("Illegal ASCII code for symbol " + sym)
wenzelm@34193
   279
          else (sym, ch)
wenzelm@34193
   280
        }
wenzelm@31545
   281
      (new Recoder(mapping),
wenzelm@31548
   282
       new Recoder(mapping map { case (x, y) => (y, x) }))
wenzelm@31522
   283
    }
wenzelm@27918
   284
wenzelm@34098
   285
    def decode(text: String): String = decoder.recode(text)
wenzelm@34098
   286
    def encode(text: String): String = encoder.recode(text)
wenzelm@34134
   287
wenzelm@43490
   288
    private def recode_set(elems: String*): Set[String] =
wenzelm@43490
   289
    {
wenzelm@43490
   290
      val content = elems.toList
wenzelm@43490
   291
      Set((content ::: content.map(decode)): _*)
wenzelm@43490
   292
    }
wenzelm@43490
   293
wenzelm@43490
   294
    private def recode_map[A](elems: (String, A)*): Map[String, A] =
wenzelm@43490
   295
    {
wenzelm@43490
   296
      val content = elems.toList
wenzelm@43490
   297
      Map((content ::: content.map({ case (sym, a) => (decode(sym), a) })): _*)
wenzelm@43490
   298
    }
wenzelm@43490
   299
wenzelm@43490
   300
wenzelm@43490
   301
    /* user fonts */
wenzelm@43490
   302
wenzelm@43696
   303
    val fonts: Map[Symbol, String] =
wenzelm@43490
   304
      recode_map((
wenzelm@43490
   305
        for ((sym, props) <- symbols if props.isDefinedAt("font"))
wenzelm@43490
   306
          yield (sym -> props("font"))): _*)
wenzelm@43490
   307
wenzelm@43490
   308
    val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
wenzelm@43490
   309
    val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
wenzelm@43490
   310
wenzelm@34134
   311
wenzelm@34134
   312
    /* classification */
wenzelm@34134
   313
wenzelm@43695
   314
    val letters = recode_set(
wenzelm@34134
   315
      "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
wenzelm@34134
   316
      "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
wenzelm@34134
   317
      "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
wenzelm@34134
   318
      "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z",
wenzelm@34134
   319
wenzelm@34134
   320
      "\\<A>", "\\<B>", "\\<C>", "\\<D>", "\\<E>", "\\<F>", "\\<G>",
wenzelm@34134
   321
      "\\<H>", "\\<I>", "\\<J>", "\\<K>", "\\<L>", "\\<M>", "\\<N>",
wenzelm@34134
   322
      "\\<O>", "\\<P>", "\\<Q>", "\\<R>", "\\<S>", "\\<T>", "\\<U>",
wenzelm@34134
   323
      "\\<V>", "\\<W>", "\\<X>", "\\<Y>", "\\<Z>", "\\<a>", "\\<b>",
wenzelm@34134
   324
      "\\<c>", "\\<d>", "\\<e>", "\\<f>", "\\<g>", "\\<h>", "\\<i>",
wenzelm@34134
   325
      "\\<j>", "\\<k>", "\\<l>", "\\<m>", "\\<n>", "\\<o>", "\\<p>",
wenzelm@34134
   326
      "\\<q>", "\\<r>", "\\<s>", "\\<t>", "\\<u>", "\\<v>", "\\<w>",
wenzelm@34134
   327
      "\\<x>", "\\<y>", "\\<z>",
wenzelm@34134
   328
wenzelm@34134
   329
      "\\<AA>", "\\<BB>", "\\<CC>", "\\<DD>", "\\<EE>", "\\<FF>",
wenzelm@34134
   330
      "\\<GG>", "\\<HH>", "\\<II>", "\\<JJ>", "\\<KK>", "\\<LL>",
wenzelm@34134
   331
      "\\<MM>", "\\<NN>", "\\<OO>", "\\<PP>", "\\<QQ>", "\\<RR>",
wenzelm@34134
   332
      "\\<SS>", "\\<TT>", "\\<UU>", "\\<VV>", "\\<WW>", "\\<XX>",
wenzelm@34134
   333
      "\\<YY>", "\\<ZZ>", "\\<aa>", "\\<bb>", "\\<cc>", "\\<dd>",
wenzelm@34134
   334
      "\\<ee>", "\\<ff>", "\\<gg>", "\\<hh>", "\\<ii>", "\\<jj>",
wenzelm@34134
   335
      "\\<kk>", "\\<ll>", "\\<mm>", "\\<nn>", "\\<oo>", "\\<pp>",
wenzelm@34134
   336
      "\\<qq>", "\\<rr>", "\\<ss>", "\\<tt>", "\\<uu>", "\\<vv>",
wenzelm@34134
   337
      "\\<ww>", "\\<xx>", "\\<yy>", "\\<zz>",
wenzelm@34134
   338
wenzelm@34134
   339
      "\\<alpha>", "\\<beta>", "\\<gamma>", "\\<delta>", "\\<epsilon>",
wenzelm@34134
   340
      "\\<zeta>", "\\<eta>", "\\<theta>", "\\<iota>", "\\<kappa>",
wenzelm@34134
   341
      "\\<mu>", "\\<nu>", "\\<xi>", "\\<pi>", "\\<rho>", "\\<sigma>",
wenzelm@34134
   342
      "\\<tau>", "\\<upsilon>", "\\<phi>", "\\<chi>", "\\<psi>",
wenzelm@34134
   343
      "\\<omega>", "\\<Gamma>", "\\<Delta>", "\\<Theta>", "\\<Lambda>",
wenzelm@34134
   344
      "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
wenzelm@34134
   345
      "\\<Psi>", "\\<Omega>",
wenzelm@34134
   346
wenzelm@34134
   347
      "\\<^isub>", "\\<^isup>")
wenzelm@34134
   348
wenzelm@43695
   349
    val blanks =
wenzelm@43490
   350
      recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
wenzelm@34138
   351
wenzelm@43695
   352
    val sym_chars =
wenzelm@34138
   353
      Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
wenzelm@34134
   354
wenzelm@43455
   355
wenzelm@43488
   356
    /* control symbols */
wenzelm@43488
   357
wenzelm@43696
   358
    val ctrl_decoded: Set[Symbol] =
wenzelm@43488
   359
      Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
wenzelm@43488
   360
wenzelm@44238
   361
    val sub_decoded = decode("\\<^sub>")
wenzelm@44238
   362
    val sup_decoded = decode("\\<^sup>")
wenzelm@44238
   363
    val isub_decoded = decode("\\<^isub>")
wenzelm@44238
   364
    val isup_decoded = decode("\\<^isup>")
wenzelm@43511
   365
    val bsub_decoded = decode("\\<^bsub>")
wenzelm@43511
   366
    val esub_decoded = decode("\\<^esub>")
wenzelm@43511
   367
    val bsup_decoded = decode("\\<^bsup>")
wenzelm@43511
   368
    val esup_decoded = decode("\\<^esup>")
wenzelm@44238
   369
    val bold_decoded = decode("\\<^bold>")
wenzelm@27918
   370
  }
wenzelm@43695
   371
wenzelm@43695
   372
wenzelm@43695
   373
  /* tables */
wenzelm@43695
   374
wenzelm@43696
   375
  def names: Map[Symbol, String] = symbols.names
wenzelm@43696
   376
  def abbrevs: Map[Symbol, String] = symbols.abbrevs
wenzelm@43695
   377
wenzelm@43695
   378
  def decode(text: String): String = symbols.decode(text)
wenzelm@43695
   379
  def encode(text: String): String = symbols.encode(text)
wenzelm@43695
   380
wenzelm@43696
   381
  def fonts: Map[Symbol, String] = symbols.fonts
wenzelm@43695
   382
  def font_names: List[String] = symbols.font_names
wenzelm@43695
   383
  def font_index: Map[String, Int] = symbols.font_index
wenzelm@43696
   384
  def lookup_font(sym: Symbol): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
wenzelm@43695
   385
wenzelm@43695
   386
wenzelm@43695
   387
  /* classification */
wenzelm@43695
   388
wenzelm@43696
   389
  def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym)
wenzelm@43696
   390
  def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
wenzelm@43696
   391
  def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
wenzelm@43696
   392
  def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
wenzelm@43696
   393
  def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
wenzelm@43696
   394
  def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
wenzelm@43696
   395
  def is_symbolic(sym: Symbol): Boolean =
wenzelm@43695
   396
    sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
wenzelm@43695
   397
wenzelm@43695
   398
wenzelm@43695
   399
  /* control symbols */
wenzelm@43695
   400
wenzelm@43696
   401
  def is_ctrl(sym: Symbol): Boolean =
wenzelm@43695
   402
    sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
wenzelm@43695
   403
wenzelm@43696
   404
  def is_controllable(sym: Symbol): Boolean =
wenzelm@43695
   405
    !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
wenzelm@43695
   406
wenzelm@44238
   407
  def sub_decoded: Symbol = symbols.sub_decoded
wenzelm@44238
   408
  def sup_decoded: Symbol = symbols.sup_decoded
wenzelm@44238
   409
  def isub_decoded: Symbol = symbols.isub_decoded
wenzelm@44238
   410
  def isup_decoded: Symbol = symbols.isup_decoded
wenzelm@44238
   411
  def bsub_decoded: Symbol = symbols.bsub_decoded
wenzelm@44238
   412
  def esub_decoded: Symbol = symbols.esub_decoded
wenzelm@44238
   413
  def bsup_decoded: Symbol = symbols.bsup_decoded
wenzelm@44238
   414
  def esup_decoded: Symbol = symbols.esup_decoded
wenzelm@44238
   415
  def bold_decoded: Symbol = symbols.bold_decoded
wenzelm@27901
   416
}