in content/resources/js/prettify.js [265:274]
function encodeEscape(charCode) {
if (charCode < 0x20) {
return (charCode < 0x10 ? '\\x0' : '\\x') + charCode.toString(16);
}
var ch = String.fromCharCode(charCode);
if (ch === '\\' || ch === '-' || ch === '[' || ch === ']') {
ch = '\\' + ch;
}
return ch;
}