--- 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")
--- 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 != '\'')