- escaped_string+= '\\';
- switch (c) {
- case '"': escaped_string+= '"'; break;
- case '\\': escaped_string+= '\\'; break;
- case '\t': escaped_string+='t'; break;
- case '\r': escaped_string+='r'; break;
- case '\n': escaped_string+='n'; break;
- default:
- char const* const hexdig= "0123456789ABCDEF";
- escaped_string+= 'x';
- escaped_string+= hexdig[c >> 4];
- escaped_string+= hexdig[c & 0xF];
- }
+ char const* const hexdig= "0123456789ABCDEF";
+ escaped_string+= "&#x";
+ escaped_string+= hexdig[c >> 4];
+ escaped_string+= hexdig[c & 0xF];
+ escaped_string+= ';';