update in binaries for λδ

+ roles: updated web interface with filter function in js

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/Makefile b/matita/matita/contribs/lambdadelta/bin/roles/Makefile
index 23052c171f835f40954727a1746e4182409faeff..cadebda99e50cec132094484df25fc2b188f531f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/Makefile
+++ b/matita/matita/contribs/lambdadelta/bin/roles/Makefile
@@ -10,4 +10,7 @@ test:
 up-css:
        @scp roles.css lahar.helm.cs.unibo.it:/projects/helm/public_html/lambdadelta/css/
 
-.PHONY: test up-css
+up-js:
+       @scp roles.js lahar.helm.cs.unibo.it:/projects/helm/public_html/lambdadelta/js/
+
+.PHONY: test up-css up-js

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/roles.css b/matita/matita/contribs/lambdadelta/bin/roles/roles.css
index ecb9a078cfd4ae2c4a6938d2a6d2d3fe8d536cf9..80db3a4c35265c8193df4f74b2f2f1b20ff7e127 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/roles.css
+++ b/matita/matita/contribs/lambdadelta/bin/roles/roles.css
@@ -95,6 +95,13 @@ a:active {
 .count {
 }
 
+.filter {
+}
+
+.hidden {
+  display: none;
+}
+
 .selected {
   border: 1pt solid;
 }

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/roles.js b/matita/matita/contribs/lambdadelta/bin/roles/roles.js
new file mode 100644 (file)
index 0000000..c93e6d0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/roles/roles.js
@@ -0,0 +1,11 @@
+function filter(ptr) {
+  var query = document.getElementById('f.'+ptr).value;
+  var cl = document.getElementsByName(ptr);
+  for (i=0;i < cl.length; i++) {
+    if (cl[i].getAttribute('key').search(query) >= 0) {
+      cl[i].classList.remove('hidden')
+    } else {
+      cl[i].classList.add('hidden')
+    }
+  }
+}

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
index cb204a9afb220d3af2d583285754e3a399cca460..0f1aedd4a4eb5a8310ef56c15c18ad7bd3482758 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
@@ -138,12 +138,12 @@ let visit_status
   let visit_r p r =
     before r.ET.rx (r.ET.ro=[]) (r.ET.rn=[]);
     if r.ET.rx then begin
-      EU.list_visit before_t each_t visit_tw after_t EU.oobj_selected EU.string_of_oobj (1::p) r.ET.ro;
-      EU.list_visit before_w each_w visit_tw after_w EU.nobj_selected EU.string_of_nobj (2::p) r.ET.rn
+      EU.list_visit before_t each_t visit_tw after_t EU.oobj_selected EU.key_of_oobj EU.string_of_oobj (1::p) r.ET.ro;
+      EU.list_visit before_w each_w visit_tw after_w EU.nobj_selected EU.key_of_nobj EU.string_of_nobj (2::p) r.ET.rn
     end;
     after r.ET.rx
   in
-  EU.list_visit before_r each_r visit_r after_r EU.robj_selected EU.string_of_robj [0] st.ET.sr;
+  EU.list_visit before_r each_r visit_r after_r EU.robj_selected EU.key_of_robj EU.string_of_robj [0] st.ET.sr;
   stage (EU.string_of_stage st.ET.ss) st.ET.sm;
-  EU.list_visit before_t each_t visit_tw after_t EU.oobj_selected EU.string_of_oobj [1] st.ET.so;
-  EU.list_visit before_w each_w visit_tw after_w EU.nobj_selected EU.string_of_nobj [2] st.ET.sn
+  EU.list_visit before_t each_t visit_tw after_t EU.oobj_selected EU.key_of_oobj EU.string_of_oobj [1] st.ET.so;
+  EU.list_visit before_w each_w visit_tw after_w EU.nobj_selected EU.key_of_nobj EU.string_of_nobj [2] st.ET.sn

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli
index c7ecaf5388212db109e07e39317e05ebe5f009fe..ef63730e22b3441d28eae6852741189b06c967ef 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli
@@ -32,9 +32,9 @@ val write_status: unit -> unit
 val print_status: unit -> unit
 
 val visit_status:
-  (string -> string -> unit) -> (string -> bool -> string -> unit) ->
+  (string -> string -> unit) -> RolesTypes.each ->
   (bool -> bool -> bool -> unit) -> (bool -> unit) -> (unit -> unit) ->
   (string -> bool -> unit) ->
-  (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
-  (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
+  (string -> string -> unit) -> RolesTypes.each -> (unit -> unit) ->
+  (string -> string -> unit) -> RolesTypes.each -> (unit -> unit) ->
   unit

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesTypes.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesTypes.ml
index f57d17641e04466ccd27898f20b0875ab49d7c36..301142f7f94cdf63ac7688b431d2d3f1226db9db 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesTypes.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesTypes.ml
@@ -62,3 +62,5 @@ type error = EWrongExt of string
            | EWrongRequest of string * string
 
 exception Error of error
+
+type each = string -> string -> bool -> string -> string -> unit

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
index aeeee5f55536dec36da30cbb1e5a02659a4623d4..a67c8ea93cedfb492c659b2c354cd60f9851ec07 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
@@ -88,6 +88,8 @@ let nobj_of_string s = {
   ET.nb = false; ET.nn = name_of_string s;
 }
 
+let key_of_nobj n = string_of_nobj n
+
 let nobj_selected n = n.ET.nb
 
 let nobj_select n =
@@ -110,6 +112,8 @@ let oobj_of_string s =
   | [ss;sn] -> {ET.ob = false; ET.os = stage_of_string ss; ET.on = name_of_string sn}
   | _       -> failwith "oobj_of_string"
 
+let key_of_oobj o = string_of_name o.ET.on
+
 let oobj_selected o = o.ET.ob
 
 let oobj_select o =
@@ -148,6 +152,8 @@ let oobj_of_robj r =
 let string_of_robj r =
   string_of_oobj (oobj_of_robj r)
 
+let key_of_robj r = key_of_oobj (oobj_of_robj r)
+
 let robj_selected r = r.ET.rb
 
 let robj_select r =
@@ -201,12 +207,12 @@ let string_of_pointer = string_of_stage
 
 let pointer_of_string = stage_of_string
 
-let list_visit before each visit after selected string_of p l =
+let list_visit before each visit after selected key_of string_of p l =
   let ptr p = string_of_pointer (List.rev p) in
   let rec aux i = function
     | []      -> ()
     | x :: tl ->
-      each (ptr (i::p)) (selected x) (string_of x);
+      each (ptr p) (ptr (i::p)) (selected x) (key_of x) (string_of x);
       visit (i::p) x;
       aux (succ i) tl
   in

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli
index 55d159cd2646ed0621360b9693644a5fcb17a373..5317c51017a9d029e8c94330e623da036772937a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli
@@ -18,9 +18,9 @@ val list_nth: ('a -> unit) -> int -> 'a list -> unit
 val list_split: ('a -> bool) -> ('a -> unit) -> 'a list -> 'a list * 'a list
 
 val list_visit:
-  (string -> string -> unit) -> (string -> bool -> string -> unit) ->
+  (string -> string -> unit) -> RolesTypes.each ->
   (RolesTypes.pointer -> 'a -> unit) -> (unit -> unit) ->
-  ('a -> bool) -> ('a -> string) -> RolesTypes.pointer -> 'a list -> unit
+  ('a -> bool) -> ('a -> string) -> ('a -> string) -> RolesTypes.pointer -> 'a list -> unit
 
 val string_of_stage: RolesTypes.stage -> string
 
@@ -32,6 +32,8 @@ val string_of_nobj: RolesTypes.nobj -> string
 
 val nobj_of_string: string -> RolesTypes.nobj
 
+val key_of_nobj: RolesTypes.nobj -> string
+
 val nobj_selected: RolesTypes.nobj -> bool
 
 val nobj_select: RolesTypes.nobj -> unit
@@ -42,6 +44,8 @@ val string_of_oobj: RolesTypes.oobj -> string
 
 val oobj_of_string: string -> RolesTypes.oobj
 
+val key_of_oobj: RolesTypes.oobj -> string
+
 val oobj_selected: RolesTypes.oobj -> bool
 
 val oobj_select: RolesTypes.oobj -> unit
@@ -52,6 +56,8 @@ val oobj_match: int -> int -> RolesTypes.oobjs -> RolesTypes.nobjs -> (int * int
 
 val string_of_robj: RolesTypes.robj -> string
 
+val key_of_robj: RolesTypes.robj -> string
+
 val robj_selected: RolesTypes.robj -> bool
 
 val robj_select: RolesTypes.robj -> unit

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
index db9d007923edee60d73781dc3b17c1c984ffd80d..4905661fea43feaa8360a95a66bda04eaaa59937 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
@@ -23,9 +23,10 @@ let open_out () =
   let author = "λδ development binary: role manager" in
   let description = "λδ development binary: role manager" in
   let title = "Role Manager" in
-  let css = Filename.concat !EG.base_url "css/roles.css" in
   let icon = Filename.concat !EG.base_url "images/crux_32.ico" in
-  WS.open_out_html author description title css icon
+  let css = Filename.concat !EG.base_url "css/roles.css" in
+  let js = Filename.concat !EG.base_url "js/roles.js" in
+  WS.open_out_html author description title icon css js
 
 let close_out () =
   WS.close_out_html ()
@@ -34,6 +35,10 @@ let string_of_request req arg =
   WS.string_of_request "roles" (["system-"^req, arg], "")
 
 let status_out () =
+  let filter p =
+    KP.printf "<input class=\"filter\" type=\"text\" placeholder=\"Filter...\" \
+      onkeyup=\"filter('%s');\" id=\"f.%s\"\n/>" p p 
+  in
   let button_specs = [
     "default", "Refresh";
     "save", "Save";
@@ -49,13 +54,14 @@ let status_out () =
     let req = string_of_request "select" p in
     KP.printf "<div class=\"roles-head role-color\">\n";
     KP.printf "<a href=\"%s\">Roles:</a>\n" req;
-    KP.printf "<span class=\"count\">%s</span>\n" count
+    KP.printf "<span class=\"count\">%s</span>\n" count;
+    filter p
   in
-  let each_role p b str =
+  let each_role n p b k str =
     let req_x = string_of_request "expand" p in
     let req_s = string_of_request "select" p in
     let s = if b then " selected" else "" in
-    KP.printf "<div class=\"role role-color%s\">" s;
+    KP.printf "<div class=\"role role-color%s\" name=%S key=%S>" s n k;
     KP.printf "<a href=\"%s\">⮞</a> " req_x;
     KP.printf "<a href=\"%s\">%s</a>" req_s str
   in
@@ -89,14 +95,16 @@ let status_out () =
     KP.printf "<div class=\"atoms-head %s\">\n" c;
     KP.printf "<a href=\"%s\">%s:</a>\n" req str;
     KP.printf "<span class=\"count\">%s</span>\n" count;
+    filter p;
     KP.printf "</div>\n";
     KP.printf "<div class=\"atoms\"><table class=\"atoms-table\"><tr>\n"
   in
-  let each_atom a p b str =
+  let each_atom a n p b k str =
     let c = if a then "object-color" else "name-color" in
     let s = if b then " selected" else "" in
     let req = string_of_request "select" p in
-    KP.printf "<td class=\"atom %s%s\"><a href=\"%s\">%s</a></td>\n" c s req str
+    KP.printf "<td class=\"atom %s%s\" name=%S key=%S>\
+      <a href=\"%s\">%s</a></td>\n" c s n k req str
   in
   let after_atoms () =
     KP.printf "</tr></table></div>\n"

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webLWS.ml b/matita/matita/contribs/lambdadelta/bin/roles/webLWS.ml
index 89dbfb5d2747cd316633b1c9e54e4fbf0e5cc310..35b658a1fed2833a921ff76da8a9562b1e843964 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/webLWS.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/webLWS.ml
@@ -62,7 +62,7 @@ let control_input form =
   KP.printf "<input form=\"%s\" type=\"hidden\" name=\"%s\" value=\"%s\"/>"
     form "control-random" (get_random ())
 
-let open_out_html author description title css icon =
+let open_out_html author description title icon css js =
   open_out "application/xhtml+xml" 0;
   KP.printf "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n";
   KP.printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.1//EN\" \"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd\">\n";
@@ -74,13 +74,15 @@ let open_out_html author description title css icon =
   KP.printf "  <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\"/>\n";
   KP.printf "  <meta http-equiv=\"Content-Language\" content=\"en-us\"/>\n";
   KP.printf "  <meta http-equiv=\"Content-Style-Type\" content=\"text/css\"/>\n";
+  KP.printf "  <meta http-equiv=\"content-script-type\" content=\"text/javascript\"/>\n";
   KP.printf "  <meta name=\"author\" content=\"%s\"/>\n" author;
   KP.printf "  <meta name=\"description\" content=\"%s\"/>\n" description;
   KP.printf "  <title>%s</title>" title;
-  KP.printf "  <link rel=\"stylesheet\" type=\"text/css\" href=\"%s\"/>\n" css;
   KP.printf "  <link rel=\"shortcut icon\" href=\"%s\"/>\n" icon;
+  KP.printf "  <link rel=\"stylesheet\" type=\"text/css\" href=\"%s\"/>\n" css;
   KP.printf "</head>\n";
-  KP.printf "<body lang=\"en-US\">\n"
+  KP.printf "<body lang=\"en-US\">\n";
+  KP.printf "<script type=\"text/javascript\" src=\"%s\"/>\n" js
 
 let close_out_html () =
   KP.printf "</body>\n";

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webLWS.mli b/matita/matita/contribs/lambdadelta/bin/roles/webLWS.mli
index 7601610b067c4be6929a485eedfb10c04c55002a..5cd3af578aab3c404220c016ba851151c7821c0f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/webLWS.mli
+++ b/matita/matita/contribs/lambdadelta/bin/roles/webLWS.mli
@@ -21,6 +21,6 @@ val string_of_request: string -> request -> string
 
 val control_input: string -> unit
 
-val open_out_html: string -> string -> string -> string -> string -> unit
+val open_out_html: string -> string -> string -> string -> string -> string -> unit
 
 val close_out_html: unit -> unit