function highlight_menu(menuid, dselected){
	var menuitems = document.getElementById(menuid).getElementsByTagName("a")
	for (var i = 0; i < menuitems.length; ++i){
		if (parseInt(dselected)==i) {
			menuitems[i].parentNode.className+=" header_menu_selected "
		}
	}
}

