function highlight(name) {
	document.getElementById(name).innerHTML="<font style='color: red'>[</font> "+name+" <font style='color: red'>]</font>";
}

function remove(name) {
	document.getElementById(name).innerHTML=""+name+"";
}