--- a/src/Pure/General/json.scala Fri Oct 27 11:46:03 2017 +0200
+++ b/src/Pure/General/json.scala Fri Oct 27 13:50:08 2017 +0200
@@ -53,10 +53,7 @@
/* keyword */
def keyword: Parser[Token] =
- elem("keyword", "{}[],:".contains(_)) ^^ (c => Token(Kind.KEYWORD, c.toString)) |
- letters1 ^^ (s =>
- if (s == "true" || s == "false" || s == "null") Token(Kind.KEYWORD, s)
- else errorToken("Bad keyword: " + quote(s)))
+ (letters1 | one(character("{}[],:".contains(_)))) ^^ (s => Token(Kind.KEYWORD, s))
/* string */