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