diff -r b3f6e81cd13b -r afd657fffdf9 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Jul 11 19:03:08 2016 +0200
+++ b/src/Pure/Isar/token.scala	Mon Jul 11 20:37:28 2016 +0200
@@ -228,6 +228,8 @@
   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_keyword(name: Char): Boolean =
+    kind == Token.Kind.KEYWORD && source.length == 1 && source(0) == 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
@@ -256,6 +258,9 @@
     source.startsWith(Symbol.open) ||
     source.startsWith(Symbol.open_decoded))
 
+  def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword(_))
+  def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword(_))
+
   def is_begin: Boolean = is_keyword("begin")
   def is_end: Boolean = is_command("end")