src/Pure/General/symbol.scala
author wenzelm
Thu, 24 May 2012 22:07:00 +0200
changeset 47993 135fd6f2dadd
parent 47121 fb5764df8a9c
child 48277 f14e564fca1a
permissions -rw-r--r--
less warning in scala-2.10.0-M3;

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