--- a/src/Pure/Isar/token.scala Sun Mar 15 12:49:20 2015 +0100
+++ b/src/Pure/Isar/token.scala Sun Mar 15 14:46:01 2015 +0100
@@ -212,8 +212,7 @@
{
def is_command: Boolean = kind == Token.Kind.COMMAND
def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
- is_command &&
- (keywords.command_kind(source) match { case Some(k) => pred(k) case None => false })
+ is_command && keywords.is_command_kind(source, pred)
def is_keyword: Boolean = kind == Token.Kind.KEYWORD
def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
def is_ident: Boolean = kind == Token.Kind.IDENT