function high(name) { $(name).getChildren().setStyle('background', '#DDEECC'); }
function unhigh(name) { $(name).getChildren().setStyle('background', '#FFFFFF'); }