function highlight_on(x)
{
	x.style.background='#DDDBDB';
	x.style.border='1px solid #C16100';
}

function highlight_off(x)
{
	x.style.background='';
	x.style.border='1px solid #6B6B6B';
}