Subject: json-encode-string incorrectly encodes extra-BMP characters

From: Nathan Trapuzzano <[email-masked]>
Date: Fri, 28 Mar 2014 18:22:25 -0400

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".