# HG changeset patch
# User wenzelm
# Date 1509105008 -7200
# Node ID b4d4027f743b83da2726e470176c07402e8541bd
# Parent  914935f8a462515c86a10e706e00a56b166316aa
more permissive;

diff -r 914935f8a462 -r b4d4027f743b src/Pure/General/json.scala
--- 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 */