changeset 47012 | 0e246130486b |
parent 46943 | ac1c41ea856d |
child 48335 | 2f923e994056 |
--- a/src/Pure/Isar/token.scala Sun Mar 18 22:09:00 2012 +0100 +++ b/src/Pure/Isar/token.scala Mon Mar 19 14:59:31 2012 +0100 @@ -81,6 +81,7 @@ def is_space: Boolean = kind == Token.Kind.SPACE def is_comment: Boolean = kind == Token.Kind.COMMENT def is_ignored: Boolean = is_space || is_comment + def is_unparsed: Boolean = kind == Token.Kind.UNPARSED def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin" def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"