src/Pure/General/json.scala
changeset 78920 e495f910dd94
parent 78597 ecf0b65ada9e
child 80441 c420429fdf4c
equal deleted inserted replaced
78919:7847cbfe3a62 78920:e495f910dd94
    84 
    84 
    85     def string_escape: Parser[Char] =
    85     def string_escape: Parser[Char] =
    86       elem("", "\"\\/".contains(_)) |
    86       elem("", "\"\\/".contains(_)) |
    87       elem("", "bfnrt".contains(_)) ^^
    87       elem("", "bfnrt".contains(_)) ^^
    88         { case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } |
    88         { case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } |
    89       'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^
    89       'u' ~> repeated(character(Symbol.is_ascii_hex), 4, 4) ^^
    90         (s => Integer.parseInt(s, 16).toChar)
    90         (s => Integer.parseInt(s, 16).toChar)
    91 
    91 
    92     def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string")
    92     def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string")
    93 
    93 
    94 
    94