more accurate JSON parsing according to http://seriot.ch/parsing_json.php
authorwenzelm
Fri Dec 01 18:20:15 2017 +0100 (7 weeks ago)
changeset 6711142f290d8ccbd
parent 67110 3156faac30a7
child 67112 deb2fcbda16e
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
src/Pure/General/json.scala
     1.1 --- a/src/Pure/General/json.scala	Fri Dec 01 16:58:26 2017 +0100
     1.2 +++ b/src/Pure/General/json.scala	Fri Dec 01 18:20:15 2017 +0100
     1.3 @@ -44,8 +44,9 @@
     1.4  
     1.5      def errorToken(msg: String): Token = Token(Kind.ERROR, msg)
     1.6  
     1.7 -    override val whiteSpace = """\s+""".r
     1.8 -    def whitespace: Parser[Any] = many(character(Symbol.is_ascii_blank(_)))
     1.9 +    val white_space: String = " \t\n\r"
    1.10 +    override val whiteSpace = ("[" + white_space + "]+").r
    1.11 +    def whitespace: Parser[Any] = many(character(white_space.contains(_)))
    1.12  
    1.13      val letter: Parser[String] = one(character(Symbol.is_ascii_letter(_)))
    1.14      val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter(_)))
    1.15 @@ -66,7 +67,7 @@
    1.16        '\"' ~> rep(string_body) <~ '\"' ^^ (cs => Token(Kind.STRING, cs.mkString))
    1.17  
    1.18      def string_body: Parser[Char] =
    1.19 -      elem("", c => c != '\"' && c != '\\' && c != EofCh) | '\\' ~> string_escape
    1.20 +      elem("", c => c > '\u001f' && c != '\"' && c != '\\' && c != EofCh) | '\\' ~> string_escape
    1.21  
    1.22      def string_escape: Parser[Char] =
    1.23        elem("", "\"\\/".contains(_)) |
    1.24 @@ -81,7 +82,7 @@
    1.25      /* number */
    1.26  
    1.27      def number: Parser[Token] =
    1.28 -      opt("-" <~ whitespace) ~ number_body ~ opt(letter) ^^ {
    1.29 +      opt("-") ~ number_body ~ opt(letter) ^^ {
    1.30          case a ~ b ~ None => Token(Kind.NUMBER, a.getOrElse("") + b)
    1.31          case a ~ b ~ Some(c) =>
    1.32            errorToken("Invalid number format: " + quote(a.getOrElse("") + b + c))