function trim(s)
{
	if (s == null || s == "") {return "";}
	return s.replace(/^\s*/,"").replace(/\s*$/,"");
}

function htmlentities(str)
{
	return str.replace(/&lt;/g,"<").replace(/&gt;/g,">");
}