src/Pure/Isar/token.scala

--- a/src/Pure/Isar/token.scala	Mon Jul 11 17:53:02 2016 +0200
+++ b/src/Pure/Isar/token.scala	Mon Jul 11 18:18:24 2016 +0200
@@ -225,7 +225,9 @@
 sealed case class Token(kind: Token.Kind.Value, source: String)
 {
   def is_command: Boolean = kind == Token.Kind.COMMAND
+  def is_command(name: String): Boolean = kind == Token.Kind.COMMAND && source == name
   def is_keyword: Boolean = kind == Token.Kind.KEYWORD
+  def is_keyword(name: String): Boolean = kind == Token.Kind.KEYWORD && source == name
   def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
   def is_ident: Boolean = kind == Token.Kind.IDENT
   def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT
@@ -254,8 +256,8 @@
     source.startsWith(Symbol.open) ||
     source.startsWith(Symbol.open_decoded))
 
-  def is_begin: Boolean = is_keyword && source == "begin"
-  def is_end: Boolean = is_command && source == "end"
+  def is_begin: Boolean = is_keyword("begin")
+  def is_end: Boolean = is_command("end")
 
   def content: String =
     if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)