function highlight(obj) {
    obj.className=obj.className + " white";
}
function unhighlight(obj) {
  obj.className=obj.className.replace(" white", "");
}