rot13 = {

	convert: function(a) {
		return a.replace(/[a-zA-Z]/g, function(c){return String.fromCharCode
		((c<="Z"?90:122)>=(c=c.charCodeAt(0)+13)?c:c-26);});
	},

	write: function(a) {
		document.write(rot13.convert(a));
	},

	mailto: function(a) {
		var match=/(.*)(@.*)/.exec(a);
		var s=rot13.convert(match[1])+match[2];
		document.write('<a href="mailto:'+s+'">'+s+'</a>');
	}

}