document.selection.text = document.selection.text.replace(/&#x([0-9a-f]{1,6});/gi,function (b,c){return String.fromCharCode(dec(c.length-1,1,c.toUpperCase()))});
function dec(d,e,c)
	{return ('0123456789ABCDEF').indexOf(c.substring(d))*e + ((d == 0)?0:dec(d-1,e*16,c.substring(0,d)));}