//////////////////////////////////////////////////////////////////////////////////
// ------------------------------------------------------------------------------
// function trim(s)
// Returns the string s with leading and trailing whitespace removed.
// If s is null then an empty string is returned.
// ------------------------------------------------------------------------------
//////////////////////////////////////////////////////////////////////////////////
function trim(s) {
	if (s == null) {
		return "";
	}
	var temp = s.toString();
	var len = temp.length;
	var i;
	for (i = 0; i < len; i++) {
		if (isWhitespace(temp.charCodeAt(i))) {
			temp = temp.substring(i + 1);
		}
	}
	if ( (len = temp.length) == 0 ) {
		return temp;
	}
	for (i = len - 1; i >= 0; i--) {
		if (isWhitespace(temp.charCodeAt(i))) {
			temp = temp.substring(0, i);
		}
	}
	return temp;
}

//////////////////////////////////////////////////////////////////////////////////////
// ----------------------------------------------------------------------------------
// function isWhitespace(c)
// Returns true if the character code c is a whitespace character, or false otherwise.
// ----------------------------------------------------------------------------------
//////////////////////////////////////////////////////////////////////////////////////
function isWhitespace(c) {
	return (c <= ' ' || c >= 127);
}