// elements that have the old magic IDs.
var ids = [ "Switch", "Lang", "Search", "Pager", "Navi",
"Results", "Records", "Targets", "Ranking",
// elements that have the old magic IDs.
var ids = [ "Switch", "Lang", "Search", "Pager", "Navi",
"Results", "Records", "Targets", "Ranking",