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

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