function set_backg_on(id) {
     document.getElementById(id).style.backgroundColor="#C0FFC0";
}
function set_backg_off(id) {
     document.getElementById(id).style.backgroundColor="";
}
function load_page(myurl)
{
    //  This version does NOT cause an entry in the browser's
    //  page view history.  Most browsers will always retrieve
    //  the document from the web-server whether it is already
    //  in the browsers page-cache or not.
    //  
    window.location.replace( myurl );
}