/* Adds a id 'framed' to the body node if the page is framed. This is equivalent to: This way the css style 'framed' can give a different appearance to the page. */ window.onload = function() { if (parent.location.href != self.location.href) { // page is framed // set body id to 'framed': // to address css style 'framed' // so that the margins can be defined differently var bodyNode = document.getElementsByTagName('body')[0]; bodyNode.setAttribute("id", "framed"); } } /* Loads the frameset, passing the current page url as parameter so this page can be loaded into the frame classFrame. */ function showTOC() { parent.location = "index.html?" + self.location.href; } /* Replaces the frameset by the current page. */ function hideTOC() { parent.location = self.location; }