src/Pure/Isar/token.scala
author wenzelm
Mon Nov 14 16:52:19 2011 +0100 (2011-11-14 ago)
changeset 45488 6d71d9e52369
parent 43611 21a57a0c5f25
child 46943 ac1c41ea856d
permissions -rw-r--r--
pass positions for named targets, for formal links in the document model;
wenzelm@36956
     1
/*  Title:      Pure/Isar/token.scala
wenzelm@34139
     2
    Author:     Makarius
wenzelm@34139
     3
wenzelm@36956
     4
Outer token syntax for Isabelle/Isar.
wenzelm@34139
     5
*/
wenzelm@34139
     6
wenzelm@34139
     7
package isabelle
wenzelm@34139
     8
wenzelm@34139
     9
wenzelm@36956
    10
object Token
wenzelm@34139
    11
{
wenzelm@34157
    12
  /* tokens */
wenzelm@34139
    13
wenzelm@36956
    14
  object Kind extends Enumeration
wenzelm@34139
    15
  {
wenzelm@34157
    16
    val COMMAND = Value("command")
wenzelm@34157
    17
    val KEYWORD = Value("keyword")
wenzelm@34157
    18
    val IDENT = Value("identifier")
wenzelm@34157
    19
    val LONG_IDENT = Value("long identifier")
wenzelm@34157
    20
    val SYM_IDENT = Value("symbolic identifier")
wenzelm@34157
    21
    val VAR = Value("schematic variable")
wenzelm@34157
    22
    val TYPE_IDENT = Value("type variable")
wenzelm@34157
    23
    val TYPE_VAR = Value("schematic type variable")
wenzelm@40290
    24
    val NAT = Value("natural number")
wenzelm@40290
    25
    val FLOAT = Value("floating-point number")
wenzelm@34157
    26
    val STRING = Value("string")
wenzelm@34157
    27
    val ALT_STRING = Value("back-quoted string")
wenzelm@34157
    28
    val VERBATIM = Value("verbatim text")
wenzelm@34157
    29
    val SPACE = Value("white space")
wenzelm@34157
    30
    val COMMENT = Value("comment text")
wenzelm@34157
    31
    val UNPARSED = Value("unparsed input")
wenzelm@34139
    32
  }
wenzelm@34139
    33
wenzelm@34157
    34
wenzelm@34157
    35
  /* token reader */
wenzelm@34139
    36
wenzelm@34157
    37
  class Line_Position(val line: Int) extends scala.util.parsing.input.Position
wenzelm@34139
    38
  {
wenzelm@34157
    39
    def column = 0
wenzelm@34157
    40
    def lineContents = ""
wenzelm@34157
    41
    override def toString = line.toString
wenzelm@34157
    42
wenzelm@34157
    43
    def advance(token: Token): Line_Position =
wenzelm@34157
    44
    {
wenzelm@34157
    45
      var n = 0
wenzelm@34157
    46
      for (c <- token.content if c == '\n') n += 1
wenzelm@34157
    47
      if (n == 0) this else new Line_Position(line + n)
wenzelm@34157
    48
    }
wenzelm@34139
    49
  }
wenzelm@34139
    50
wenzelm@34157
    51
  abstract class Reader extends scala.util.parsing.input.Reader[Token]
wenzelm@34157
    52
wenzelm@34157
    53
  private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader
wenzelm@34139
    54
  {
wenzelm@34157
    55
    def first = tokens.head
wenzelm@34157
    56
    def rest = new Token_Reader(tokens.tail, pos.advance(first))
wenzelm@34157
    57
    def atEnd = tokens.isEmpty
wenzelm@34139
    58
  }
wenzelm@34139
    59
wenzelm@34157
    60
  def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1))
wenzelm@34139
    61
}
wenzelm@34139
    62
wenzelm@36956
    63
wenzelm@36956
    64
sealed case class Token(val kind: Token.Kind.Value, val source: String)
wenzelm@36956
    65
{
wenzelm@36956
    66
  def is_command: Boolean = kind == Token.Kind.COMMAND
wenzelm@43430
    67
  def is_operator: Boolean = kind == Token.Kind.KEYWORD && !Symbol.is_ascii_identifier(source)
wenzelm@36956
    68
  def is_delimited: Boolean =
wenzelm@36956
    69
    kind == Token.Kind.STRING ||
wenzelm@36956
    70
    kind == Token.Kind.ALT_STRING ||
wenzelm@36956
    71
    kind == Token.Kind.VERBATIM ||
wenzelm@36956
    72
    kind == Token.Kind.COMMENT
wenzelm@36956
    73
  def is_name: Boolean =
wenzelm@36956
    74
    kind == Token.Kind.IDENT ||
wenzelm@36956
    75
    kind == Token.Kind.SYM_IDENT ||
wenzelm@36956
    76
    kind == Token.Kind.STRING ||
wenzelm@36956
    77
    kind == Token.Kind.NAT
wenzelm@36956
    78
  def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
wenzelm@36956
    79
  def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
wenzelm@36956
    80
  def is_space: Boolean = kind == Token.Kind.SPACE
wenzelm@36956
    81
  def is_comment: Boolean = kind == Token.Kind.COMMENT
wenzelm@36956
    82
  def is_ignored: Boolean = is_space || is_comment
wenzelm@36956
    83
wenzelm@43611
    84
  def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
wenzelm@43611
    85
  def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"
wenzelm@43611
    86
wenzelm@36956
    87
  def content: String =
wenzelm@36956
    88
    if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
wenzelm@36956
    89
    else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
wenzelm@36956
    90
    else if (kind == Token.Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source)
wenzelm@36956
    91
    else if (kind == Token.Kind.COMMENT) Scan.Lexicon.empty.comment_content(source)
wenzelm@36956
    92
    else source
wenzelm@36956
    93
wenzelm@36956
    94
  def text: (String, String) =
wenzelm@36956
    95
    if (kind == Token.Kind.COMMAND && source == ";") ("terminator", "")
wenzelm@36956
    96
    else (kind.toString, source)
wenzelm@36956
    97
}
wenzelm@36956
    98