explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;
authorwenzelm
Tue May 20 14:25:28 2014 +0200 (2014-05-20)
changeset 570216a8fd2ac6756
parent 57014 b7999893ffcc
child 57022 801c01004a21
explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;
src/Pure/Isar/token.scala
     1.1 --- a/src/Pure/Isar/token.scala	Tue May 20 09:57:10 2014 +0200
     1.2 +++ b/src/Pure/Isar/token.scala	Tue May 20 14:25:28 2014 +0200
     1.3 @@ -185,7 +185,9 @@
     1.4     (source.startsWith("\"") ||
     1.5      source.startsWith("`") ||
     1.6      source.startsWith("{*") ||
     1.7 -    source.startsWith("(*"))
     1.8 +    source.startsWith("(*") ||
     1.9 +    source.startsWith(Symbol.open) ||
    1.10 +    source.startsWith(Symbol.open_decoded))
    1.11  
    1.12    def is_begin: Boolean = is_keyword && source == "begin"
    1.13    def is_end: Boolean = is_keyword && source == "end"