clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;
authorwenzelm
Mon May 19 14:48:50 2014 +0200 (2014-05-19)
changeset 56998ebf3c9681406
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
     1.1 --- a/src/Pure/Isar/token.scala	Mon May 19 14:21:24 2014 +0200
     1.2 +++ b/src/Pure/Isar/token.scala	Mon May 19 14:48:50 2014 +0200
     1.3 @@ -173,7 +173,7 @@
     1.4      kind == Token.Kind.STRING ||
     1.5      kind == Token.Kind.NAT
     1.6    def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
     1.7 -  def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
     1.8 +  def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
     1.9    def is_space: Boolean = kind == Token.Kind.SPACE
    1.10    def is_comment: Boolean = kind == Token.Kind.COMMENT
    1.11    def is_improper: Boolean = is_space || is_comment