diff -r a1363da718aa -r b13ab7d11b90 src/Pure/Tools/check_keywords.scala --- a/src/Pure/Tools/check_keywords.scala Mon Apr 04 22:42:12 2022 +0200 +++ b/src/Pure/Tools/check_keywords.scala Mon Apr 04 23:33:14 2022 +0200 @@ -14,7 +14,7 @@ input: CharSequence, start: Token.Pos ): List[(Token, Position.T)] = { - object Parser extends Parse.Parser { + object Parsers extends Parse.Parsers { private val conflict = position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source))) private val other = token("token", _ => true) @@ -26,7 +26,7 @@ case bad => error(bad.toString) } } - Parser.result + Parsers.result } def check_keywords(