document.selection.text = document.selection.text.replace(/./g,function (c){return (c.charCodeAt(0) < 127)?c:'&#' + c.charCodeAt(0) + ';'})