op.callback.call(this,ev);
        };
        D.append(line, btn);
        if(op.hasOwnProperty('boolValue')){
          const check = D.attr(D.checkbox(1, op.boolValue()),
                                          'aria-label', op.label);
          D.append(line, check);
          check.addEventListener('click', callback);
        }
        D.append(settingsPopup.e, line);
        btn.addEventListener('click', callback);
      });
    };
    settingsPopup.installHideHandlers(false, true, true)
    /** Reminder: click-to-hide interferes with "?" embedded within
        the popup, so cannot be used together with those. Enabling
        this means, however, that tapping the menu button to toggle
        the menu cannot work because tapping the menu button while the