# HG changeset patch # User wenzelm # Date 1699466684 -3600 # Node ID e495f910dd948a32d5558c8dafa44a6b7840886f # Parent 7847cbfe3a62db22b6a5f383eafcc66c050961e5 tuned; diff -r 7847cbfe3a62 -r e495f910dd94 src/Pure/General/json.scala --- a/src/Pure/General/json.scala Wed Nov 08 16:05:22 2023 +0100 +++ b/src/Pure/General/json.scala Wed Nov 08 19:04:44 2023 +0100 @@ -86,7 +86,7 @@ elem("", "\"\\/".contains(_)) | elem("", "bfnrt".contains(_)) ^^ { case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } | - 'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^ + 'u' ~> repeated(character(Symbol.is_ascii_hex), 4, 4) ^^ (s => Integer.parseInt(s, 16).toChar) def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string") diff -r 7847cbfe3a62 -r e495f910dd94 src/Pure/General/toml.scala --- a/src/Pure/General/toml.scala Wed Nov 08 16:05:22 2023 +0100 +++ b/src/Pure/General/toml.scala Wed Nov 08 19:04:44 2023 +0100 @@ -213,8 +213,8 @@ elem("", "\"\\".contains(_)) | elem("", "btnfr".contains(_)) ^^ { case 'b' => '\b' case 't' => '\t' case 'n' => '\n' case 'f' => '\f' case 'r' => '\r' } | - ('u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) | - 'U' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 8, 8)) ^^ + ('u' ~> repeated(character(Symbol.is_ascii_hex), 4, 4) | + 'U' ~> repeated(character(Symbol.is_ascii_hex), 8, 8)) ^^ (s => java.lang.Integer.parseInt(s, 16).toChar) private def literal_string_elem: Parser[Elem] = elem("", c => !is_control(c) && c != '\'')