src/Pure/Isar/token.scala
changeset 51048 123be08eed88
parent 48754 c2c1e5944536
child 55033 8e8243975860
equal deleted inserted replaced
51047:2ad5c46bcd04 51048:123be08eed88
    87     kind == Token.Kind.NAT
    87     kind == Token.Kind.NAT
    88   def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
    88   def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
    89   def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
    89   def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
    90   def is_space: Boolean = kind == Token.Kind.SPACE
    90   def is_space: Boolean = kind == Token.Kind.SPACE
    91   def is_comment: Boolean = kind == Token.Kind.COMMENT
    91   def is_comment: Boolean = kind == Token.Kind.COMMENT
       
    92   def is_improper: Boolean = is_space || is_comment
    92   def is_proper: Boolean = !is_space && !is_comment
    93   def is_proper: Boolean = !is_space && !is_comment
    93   def is_error: Boolean = kind == Token.Kind.ERROR
    94   def is_error: Boolean = kind == Token.Kind.ERROR
    94   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
    95   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
    95 
    96 
    96   def is_unfinished: Boolean = is_error &&
    97   def is_unfinished: Boolean = is_error &&