src/Pure/Isar/token.scala
changeset 57021 6a8fd2ac6756
parent 56998 ebf3c9681406
child 58751 6de7dbaf3c44
equal deleted inserted replaced
57014:b7999893ffcc 57021:6a8fd2ac6756
   183 
   183 
   184   def is_unfinished: Boolean = is_error &&
   184   def is_unfinished: Boolean = is_error &&
   185    (source.startsWith("\"") ||
   185    (source.startsWith("\"") ||
   186     source.startsWith("`") ||
   186     source.startsWith("`") ||
   187     source.startsWith("{*") ||
   187     source.startsWith("{*") ||
   188     source.startsWith("(*"))
   188     source.startsWith("(*") ||
       
   189     source.startsWith(Symbol.open) ||
       
   190     source.startsWith(Symbol.open_decoded))
   189 
   191 
   190   def is_begin: Boolean = is_keyword && source == "begin"
   192   def is_begin: Boolean = is_keyword && source == "begin"
   191   def is_end: Boolean = is_keyword && source == "end"
   193   def is_end: Boolean = is_keyword && source == "end"
   192 
   194 
   193   def content: String =
   195   def content: String =