# HG changeset patch # User wenzelm # Date 1515955548 -3600 # Node ID e6d5547a0a9368e6503fafd49fcc4addff2d7165 # Parent 84e143e64336d47c8a2f95e417f6b2f96041ef79 clarified Token.is_text (cf. Parse.text in ML); diff -r 84e143e64336 -r e6d5547a0a93 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Sun Jan 14 19:44:49 2018 +0100 +++ b/src/Pure/Isar/token.scala Sun Jan 14 19:45:48 2018 +0100 @@ -285,7 +285,7 @@ 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_text: Boolean = is_embedded || kind == Token.Kind.VERBATIM def is_space: Boolean = kind == Token.Kind.SPACE def is_comment: Boolean = kind == Token.Kind.COMMENT def is_improper: Boolean = is_space || is_comment