function resizeElement(id,x,y)
{
var a = 30;
var b = 30;

document.getElementById(id).style.height = (y-a)+"px";
document.getElementById(id).style.width = x-b+"px";
}



function highlightText(codeBlock) {
	document.getElementById(codeBlock).focus();
	document.getElementById(codeBlock).select();
	}