// override function of same name in common.js
function show_switch2gui() {
    // Show switch to gui editor link if the browser is compatible
    if (can_use_gui_editor() == false) return;
    // instead of switch2gui, get xswitch2gui
    var switch2gui = document.getElementById('xswitch2gui')
    if (switch2gui) {
        switch2gui.style.display = 'inline';
    }
}


// get corresponding element without leading x in its name and click it
function tickle(x){
    yName = x.name.slice(1);
    y = document.getElementsByName(yName);
    y = y[0];
    y.click();
}