// Highlight navigation element.
function highlight(id) {
  document.getElementById(id).style.color='#6C012C';
  document.getElementById(id).style.fontWeight='bold';
}