function highlight( x ) {
	x.focus();
	x.select();
}