1 if (window.top.developerMode === undefined) {

     2     window.top.developerMode = false;

     3 }

     4 if (window.top.developerMode) {

     5     document.getElementById("developer-style").disabled = true;

     6 }

     7 

     8 function switchStylesheetHandler(event) { 

     9     window.top.developerMode = !(window.top.developerMode);

    10     document.getElementById("developer-style").disabled = window.top.developerMode;

    11     var b = getTargetNode(event);

    12     if (b) {

    13         b.firstChild.data = (window.top.developerMode ? "hide" : "show") + " advanced";

    14     }

    15 }

    16 

    17 function init() {

    18     var h = document.getElementById("header-links");

    19     if (h) {

    20         var b = document.createElement("button");

    21         b.appendChild(document.createTextNode((window.top.developerMode ? "hide" : "show") + " advanced"));

    22     	attachEventListener(b, "click", switchStylesheetHandler);

    23         h.insertBefore(document.createTextNode(" "), h.firstChild);

    24         h.insertBefore(b, h.firstChild);

    25     }

    26 }