function fetchElement(idref) {
	if (typeof(idref) != 'string') return idref;
    if (document.getElementById) return document.getElementById(idref);
    else if (document.all) return document.all[idref];
    else return null; }