--- a/src/Pure/Isar/token.scala Tue Oct 21 20:19:14 2014 +0200
+++ b/src/Pure/Isar/token.scala Tue Oct 21 20:44:17 2014 +0200
@@ -192,6 +192,9 @@
def is_begin: Boolean = is_keyword && source == "begin"
def is_end: Boolean = is_command && source == "end"
+ def is_begin_block: Boolean = is_command && source == "{"
+ def is_end_block: Boolean = is_command && source == "}"
+
def content: String =
if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source)