src/Pure/Isar/outer_lex.scala
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 34311 f0a6f02ad705
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
     1 /*  Title:      Pure/Isar/outer_lex.scala
     2     Author:     Makarius
     3 
     4 Outer lexical syntax for Isabelle/Isar.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Outer_Lex
    11 {
    12   /* tokens */
    13 
    14   object Token_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("number")
    25     val STRING = Value("string")
    26     val ALT_STRING = Value("back-quoted string")
    27     val VERBATIM = Value("verbatim text")
    28     val SPACE = Value("white space")
    29     val COMMENT = Value("comment text")
    30     val BAD_INPUT = Value("bad input")
    31     val UNPARSED = Value("unparsed input")
    32   }
    33 
    34   sealed case class Token(val kind: Token_Kind.Value, val source: String)
    35   {
    36     def is_command: Boolean = kind == Token_Kind.COMMAND
    37     def is_delimited: Boolean =
    38       kind == Token_Kind.STRING ||
    39       kind == Token_Kind.ALT_STRING ||
    40       kind == Token_Kind.VERBATIM ||
    41       kind == Token_Kind.COMMENT
    42     def is_name: Boolean =
    43       kind == Token_Kind.IDENT ||
    44       kind == Token_Kind.SYM_IDENT ||
    45       kind == Token_Kind.STRING ||
    46       kind == Token_Kind.NAT
    47     def is_xname: Boolean = is_name || kind == Token_Kind.LONG_IDENT
    48     def is_text: Boolean = is_xname || kind == Token_Kind.VERBATIM
    49     def is_space: Boolean = kind == Token_Kind.SPACE
    50     def is_comment: Boolean = kind == Token_Kind.COMMENT
    51     def is_ignored: Boolean = is_space || is_comment
    52     def is_unparsed: Boolean = kind == Token_Kind.UNPARSED
    53 
    54     def content: String =
    55       if (kind == Token_Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
    56       else if (kind == Token_Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
    57       else if (kind == Token_Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source)
    58       else if (kind == Token_Kind.COMMENT) Scan.Lexicon.empty.comment_content(source)
    59       else source
    60 
    61     def text: (String, String) =
    62       if (kind == Token_Kind.COMMAND && source == ";") ("terminator", "")
    63       else (kind.toString, source)
    64   }
    65 
    66 
    67   /* token reader */
    68 
    69   class Line_Position(val line: Int) extends scala.util.parsing.input.Position
    70   {
    71     def column = 0
    72     def lineContents = ""
    73     override def toString = line.toString
    74 
    75     def advance(token: Token): Line_Position =
    76     {
    77       var n = 0
    78       for (c <- token.content if c == '\n') n += 1
    79       if (n == 0) this else new Line_Position(line + n)
    80     }
    81   }
    82 
    83   abstract class Reader extends scala.util.parsing.input.Reader[Token]
    84 
    85   private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader
    86   {
    87     def first = tokens.head
    88     def rest = new Token_Reader(tokens.tail, pos.advance(first))
    89     def atEnd = tokens.isEmpty
    90   }
    91 
    92   def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1))
    93 }
    94