addEvent(window, "load", FunHighlight);
function addEvent(obj, evType, fn){
  /* adds an eventListener for browsers which support it
     Written by Scott Andrew: nice one, Scott */
  if (obj.addEventListener){
    obj.addEventListener(evType, fn, true);
    return true;
  } else if (obj.attachEvent){
	var r = obj.attachEvent("on"+evType, fn);
    return r;
  } else {
	return false;
  }
}
function FunHighlight()
{
    // We don't actually need createElement, but we do
    // need good DOM support, so this is a good check.
    if (!document.createElement) return;
    
    pres = document.getElementsByTagName("tt");
    for(var prei=0; prei < pres.length; prei++) {
        var pre = pres[prei];
        if( pre.className == "code") {
            HighlightCode(pre);
        }
    }
}