clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;
authorwenzelm
Mon, 19 May 2014 14:48:50 +0200
changeset 56998 ebf3c9681406
parent 56997 ab28906b54ae
child 56999 d926fc73b554
clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;
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