// Filter used to eliminate all but list items containing a particular string
// Written by Dr Greg Sheard (2007)

function do_filter(){
  if(document.getElementById('filter_box').value != ""){
   // Only do this if the filter box contains some text!
   $('li').hide();
   $('li').contains(document.getElementById('filter_box').value).show();
   $('ul.tabbernav>li').show();
  }
  else{
  // If the filter box is empty then show all list items
   $('li').show();
  }
 }

function clear_filter(){
  document.getElementById('filter_box').value = "";
  $('li').show();
 }