bug#17133: json-encode-string incorrectly encodes extra-BMP characters

[Simen Heggestøyl]

Nathan Trapuzzano <nbtrap@nbtrap.com> writes:
> M-: (princ (json-encode "\U0001d11e"))
> ==> "\u1d11e"  ;; should be "\ud834\udd1e" or "𝄞"
>
>>From ECMA-404:
>
>   To escape a code point that is not in the Basic Multilingual Plane,
>   the character is represented as a twelve-character sequence, encoding
>   the UTF-16 surrogate pair. So for example, a string containing only
>   the G clef character (U+1D11E) may be represented as "\uD834\uDD1E".

This seems to be working as expected in master now; (json-encode
"\U0001d11e") produces "𝄞" as described.

-- Simen