| changeset 57021 | 6a8fd2ac6756 |
| parent 56998 | ebf3c9681406 |
| child 58751 | 6de7dbaf3c44 |
--- a/src/Pure/Isar/token.scala Tue May 20 09:57:10 2014 +0200 +++ b/src/Pure/Isar/token.scala Tue May 20 14:25:28 2014 +0200 @@ -185,7 +185,9 @@ (source.startsWith("\"") || source.startsWith("`") || source.startsWith("{*") || - source.startsWith("(*")) + source.startsWith("(*") || + source.startsWith(Symbol.open) || + source.startsWith(Symbol.open_decoded)) def is_begin: Boolean = is_keyword && source == "begin" def is_end: Boolean = is_keyword && source == "end"