diff -r 16482dc641d4 -r 21a57a0c5f25 src/Pure/Isar/token.scala --- 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)