function htmlsrc(divname) {
	document.write("<p><div class=code>");
//	document.write("<blockquote>");
	document.write("<xmp>"+document.all[divname].innerHTML+"</xmp>");
//	document.write("</blockquote>");
	document.write("</div><p>");
}