function hover_off(this_element, menutype)
{
  this_element.style.backgroundColor='';
  this_element.style.color='';
}

function hover_on(this_element, menutype)
{
  if (menutype == '')
    menutype = 'left';
  if (menutype == 'left')
//    backcolor = '#F7F9FD';
    backcolor = '#EBF0FA';
  else if (menutype == 'top')
    backcolor = '#004B84';
  this_element.style.backgroundColor = backcolor;
}