update in binaries for λδ

[helm.git] / matita / matita / contribs / lambdadelta / bin / roles / roles.js

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/roles.js b/matita/matita/contribs/lambdadelta/bin/roles/roles.js
index c93e6d04d46d85ee10af1f9d06c6c052b4e5684f..b9d7fe2f298221d275c7d30d5ba4f7f07342b82b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/roles.js
+++ b/matita/matita/contribs/lambdadelta/bin/roles/roles.js
@@ -1,11 +1,15 @@
-function filter(ptr) {
+function filter(req, ptr) {
   var query = document.getElementById('f.'+ptr).value;
+  var anchor = document.getElementById('s.'+ptr);
   var cl = document.getElementsByName(ptr);
+  var s = "";
   for (i=0;i < cl.length; i++) {
     if (cl[i].getAttribute('key').search(query) >= 0) {
-      cl[i].classList.remove('hidden')
+      cl[i].classList.remove('hidden');
+      s = s + cl[i].getAttribute('ord') + ',';
     } else {
-      cl[i].classList.add('hidden')
+      cl[i].classList.add('hidden');
     }
-  }
+  };
+  anchor.setAttribute('href', req + '.' + s);
 }