# HG changeset patch
# User wenzelm
# Date 1400503730 -7200
# Node ID ebf3c96814062f972163f7e598c5050cee04fed3
# Parent  ab28906b54ae5518a5ecb8bdfc077339de1b50ae
clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;

diff -r ab28906b54ae -r ebf3c9681406 src/Pure/Isar/token.scala
--- 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