// JavaScript Document
var prev = '';
function do_highlight(name)
{
if(prev)
{
document.getElementById(prev).style.color = '#D45800';
}
document.getElementById(name).style.color = '#000000';

prev = name;
}