document.selection.text = document.selection.text.replace(/./g,	function (c){return (c.charCodeAt(0) < 127)?c:'&#x' + hex(c.charCodeAt(0)) + ';'});
function hex(d)
	{return (d==0)?'':(hex(Math.floor(d/16)) + ('0123456789ABCDEF').charAt(d%16))}