matita/matita/contribs/lambdadelta/bin/roles/roles.js

   1 function filter(ptr) {
   2   var query = document.getElementById('f.'+ptr).value;
   3   var cl = document.getElementsByName(ptr);
   4   for (i=0;i < cl.length; i++) {
   5     if (cl[i].getAttribute('key').search(query) >= 0) {
   6       cl[i].classList.remove('hidden')
   7     } else {
   8       cl[i].classList.add('hidden')
   9     }
  10   }
  11 }