The JSON specification requires control characters in strings to be escaped,
but the JSON1 extension does not do this. For example:
The output should be <nowiki><tt>["\u0001\b\t\n\f\r\u001f"]</tt></nowiki> but
the JSON1 extension leaves the characters unescaped.
This error arose because when I was coding up the JSON1 extension
I missed the part in the JSON specification that says that control
characters must be escaped. I understood the escapes to be optional
for all characters other than " and \.