--- a/src/Pure/Isar/token.scala Thu Jun 30 16:50:26 2011 +0200
+++ b/src/Pure/Isar/token.scala Thu Jun 30 19:24:09 2011 +0200
@@ -81,6 +81,9 @@
def is_comment: Boolean = kind == Token.Kind.COMMENT
def is_ignored: Boolean = is_space || is_comment
+ def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
+ def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"
+
def content: String =
if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)