# 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