src/Pure/Isar/token.scala
changeset 47012 0e246130486b
parent 46943 ac1c41ea856d
child 48335 2f923e994056
equal deleted inserted replaced
47011:1d8601c642cc 47012:0e246130486b
    79   def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
    79   def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
    80   def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
    80   def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
    81   def is_space: Boolean = kind == Token.Kind.SPACE
    81   def is_space: Boolean = kind == Token.Kind.SPACE
    82   def is_comment: Boolean = kind == Token.Kind.COMMENT
    82   def is_comment: Boolean = kind == Token.Kind.COMMENT
    83   def is_ignored: Boolean = is_space || is_comment
    83   def is_ignored: Boolean = is_space || is_comment
       
    84   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
    84 
    85 
    85   def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
    86   def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
    86   def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"
    87   def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"
    87 
    88 
    88   def content: String =
    89   def content: String =