src/Pure/Isar/token.scala
changeset 67432 e6d5547a0a93
parent 67132 336831647779
child 67439 78759a7bd874
equal deleted inserted replaced
67431:84e143e64336 67432:e6d5547a0a93
   283   def is_embedded: Boolean = is_name ||
   283   def is_embedded: Boolean = is_name ||
   284     kind == Token.Kind.CARTOUCHE ||
   284     kind == Token.Kind.CARTOUCHE ||
   285     kind == Token.Kind.VAR ||
   285     kind == Token.Kind.VAR ||
   286     kind == Token.Kind.TYPE_IDENT ||
   286     kind == Token.Kind.TYPE_IDENT ||
   287     kind == Token.Kind.TYPE_VAR
   287     kind == Token.Kind.TYPE_VAR
   288   def is_text: Boolean = is_name || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
   288   def is_text: Boolean = is_embedded || kind == Token.Kind.VERBATIM
   289   def is_space: Boolean = kind == Token.Kind.SPACE
   289   def is_space: Boolean = kind == Token.Kind.SPACE
   290   def is_comment: Boolean = kind == Token.Kind.COMMENT
   290   def is_comment: Boolean = kind == Token.Kind.COMMENT
   291   def is_improper: Boolean = is_space || is_comment
   291   def is_improper: Boolean = is_space || is_comment
   292   def is_proper: Boolean = !is_space && !is_comment
   292   def is_proper: Boolean = !is_space && !is_comment
   293   def is_error: Boolean = kind == Token.Kind.ERROR
   293   def is_error: Boolean = kind == Token.Kind.ERROR