more permissive;
authorwenzelm
Fri Oct 27 13:50:08 2017 +0200 (19 months ago)
changeset 66924b4d4027f743b
parent 66923 914935f8a462
child 66925 8b117dc73278
more permissive;
src/Pure/General/json.scala
     1.1 --- a/src/Pure/General/json.scala	Fri Oct 27 11:46:03 2017 +0200
     1.2 +++ b/src/Pure/General/json.scala	Fri Oct 27 13:50:08 2017 +0200
     1.3 @@ -53,10 +53,7 @@
     1.4      /* keyword */
     1.5  
     1.6      def keyword: Parser[Token] =
     1.7 -      elem("keyword", "{}[],:".contains(_)) ^^ (c => Token(Kind.KEYWORD, c.toString)) |
     1.8 -      letters1 ^^ (s =>
     1.9 -        if (s == "true" || s == "false" || s == "null") Token(Kind.KEYWORD, s)
    1.10 -        else errorToken("Bad keyword: " + quote(s)))
    1.11 +      (letters1 | one(character("{}[],:".contains(_)))) ^^ (s => Token(Kind.KEYWORD, s))
    1.12  
    1.13  
    1.14      /* string */