src/Pure/Isar/token.scala
changeset 47817 ac1c41ea856d
parent 44487 21a57a0c5f25
child 47888 0e246130486b
equal deleted inserted replaced
47816:f5c2d66faa04 47817:ac1c41ea856d
    68   def is_delimited: Boolean =
    68   def is_delimited: Boolean =
    69     kind == Token.Kind.STRING ||
    69     kind == Token.Kind.STRING ||
    70     kind == Token.Kind.ALT_STRING ||
    70     kind == Token.Kind.ALT_STRING ||
    71     kind == Token.Kind.VERBATIM ||
    71     kind == Token.Kind.VERBATIM ||
    72     kind == Token.Kind.COMMENT
    72     kind == Token.Kind.COMMENT
       
    73   def is_string: Boolean = kind == Token.Kind.STRING
    73   def is_name: Boolean =
    74   def is_name: Boolean =
    74     kind == Token.Kind.IDENT ||
    75     kind == Token.Kind.IDENT ||
    75     kind == Token.Kind.SYM_IDENT ||
    76     kind == Token.Kind.SYM_IDENT ||
    76     kind == Token.Kind.STRING ||
    77     kind == Token.Kind.STRING ||
    77     kind == Token.Kind.NAT
    78     kind == Token.Kind.NAT