diff -r 85bb70e1260b -r c40c2975fb02 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Mon Nov 07 19:07:30 2016 +0100 +++ b/src/Pure/Isar/token.scala Mon Nov 07 19:09:10 2016 +0100 @@ -242,6 +242,11 @@ kind == Token.Kind.SYM_IDENT || kind == Token.Kind.STRING || kind == Token.Kind.NAT + def is_embedded: Boolean = is_name || + kind == Token.Kind.CARTOUCHE || + kind == Token.Kind.VAR || + kind == Token.Kind.TYPE_IDENT || + kind == Token.Kind.TYPE_VAR def is_text: Boolean = is_name || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE def is_space: Boolean = kind == Token.Kind.SPACE def is_comment: Boolean = kind == Token.Kind.COMMENT