--- 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")