# HG changeset patch
# User wenzelm
# Date 1400588728 -7200
# Node ID 6a8fd2ac675661bd0b4644cfa35eb2a2c662792a
# Parent  b7999893ffcce9eff092d66553d4cbb92c823185
explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;

diff -r b7999893ffcc -r 6a8fd2ac6756 src/Pure/Isar/token.scala
--- 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"