src/Pure/Isar/token.scala
changeset 68729 3a02b424d5fb
parent 67895 cd00999d2d30
child 68730 0bc491938780
     1.1 --- a/src/Pure/Isar/token.scala	Tue Jul 31 21:06:09 2018 +0200
     1.2 +++ b/src/Pure/Isar/token.scala	Tue Jul 31 21:11:24 2018 +0200
     1.3 @@ -296,6 +296,7 @@
     1.4    def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT
     1.5    def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
     1.6    def is_comment: Boolean = is_informal_comment || is_formal_comment
     1.7 +  def is_ignored: Boolean = is_space || is_informal_comment
     1.8    def is_improper: Boolean = is_space || is_comment
     1.9    def is_proper: Boolean = !is_space && !is_comment
    1.10    def is_error: Boolean = kind == Token.Kind.ERROR