diff -r 7f4561d43d39 -r 5e64b7770f35 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Jul 30 12:08:25 2012 +0200
+++ b/src/Pure/Isar/token.scala	Mon Jul 30 13:42:45 2012 +0200
@@ -86,7 +86,7 @@
   def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
   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_proper: Boolean = !is_space && !is_comment
   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
 
   def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"