function trim (s) {
	return s.replace(/^\s+/, "").replace(/\s+$/, "");
}
function strip (s) {
	return trim(s).replace(/\W+/, "");
}
function sanitize (s) {
	return s.replace(/&/g, "&amp;").replace(/</g, "&lt;").replace(/>/g, "&gt;").replace(/\"/g, "&quot;");
}
function scrollToBottom (el) {
	try { $(el).scrollTop( $(el)[0].scrollHeight ) }
	catch (err) { }
}