function updateSearch() {
  var filter_text = document.getElementById("filter");
  var filter = filter_text.value.toLowerCase();

  var vars_ol = document.getElementById("vars");
  var lis = vars_ol.children;
  // the above line can be changed to vars_ol.getElementsByTagName("li") to filter child lists too
  // potential todo: implement a per-admin toggle for this

  for (var i = 0; i < lis.length; i++) {
    var li = lis[i];
    if (filter == "" || li.innerText.toLowerCase().indexOf(filter) != -1) {
      li.style.display = "block";
    } else {
      li.style.display = "none";
    }
  }
}

function selectTextField() {
  var filter_text = document.getElementById("filter");
  filter_text.focus();
  filter_text.select();
}

function loadPage(list) {
  if (list.options[list.selectedIndex].value == "") {
    return;
  }

  location.href = list.options[list.selectedIndex].value;
  list.selectedIndex = 0;
}