clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;
--- a/src/Pure/Isar/token.scala Mon May 19 14:21:24 2014 +0200
+++ b/src/Pure/Isar/token.scala Mon May 19 14:48:50 2014 +0200
@@ -173,7 +173,7 @@
kind == Token.Kind.STRING ||
kind == Token.Kind.NAT
def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
- def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
+ def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
def is_space: Boolean = kind == Token.Kind.SPACE
def is_comment: Boolean = kind == Token.Kind.COMMENT
def is_improper: Boolean = is_space || is_comment