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