function Plusify(string) {
	max = string.length;
	result = "";
	for (i = 0; i < max; ++i) {
		result += (string.charAt(i) == " ") ? "+" : string.charAt(i);
	}
	return result;
}

function GoSearch(ctrl,returnfile) {
	document.terms.ctrlfile.value = ctrl;
	document.terms.action = returnfile;
	setTimeout('document.terms.submit()',0);
}

function GoENC() {
	document.enc.KEYWORD.value = document.terms.textsearch.value;
	setTimeout('document.enc.submit()',0);
}