From 59fd7b5ea24e71b47aee069440f140bcccf1292a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 11 Feb 2020 19:35:15 +0100 Subject: [PATCH] =?utf8?q?update=20in=20binaries=20for=20=CE=BB=CE=B4?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + roles: updated web interface with filter function in js --- .../contribs/lambdadelta/bin/roles/Makefile | 5 ++++- .../contribs/lambdadelta/bin/roles/roles.css | 7 ++++++ .../contribs/lambdadelta/bin/roles/roles.js | 11 ++++++++++ .../lambdadelta/bin/roles/rolesEngine.ml | 10 ++++----- .../lambdadelta/bin/roles/rolesEngine.mli | 6 ++--- .../lambdadelta/bin/roles/rolesTypes.ml | 2 ++ .../lambdadelta/bin/roles/rolesUtils.ml | 10 +++++++-- .../lambdadelta/bin/roles/rolesUtils.mli | 10 +++++++-- .../lambdadelta/bin/roles/webEngine.ml | 22 +++++++++++++------ .../contribs/lambdadelta/bin/roles/webLWS.ml | 8 ++++--- .../contribs/lambdadelta/bin/roles/webLWS.mli | 2 +- 11 files changed, 69 insertions(+), 24 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/bin/roles/roles.js diff --git a/matita/matita/contribs/lambdadelta/bin/roles/Makefile b/matita/matita/contribs/lambdadelta/bin/roles/Makefile index 23052c171..cadebda99 100644 --- 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 ecb9a078c..80db3a4c3 100644 --- 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 index 000000000..c93e6d04d --- /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 cb204a9af..0f1aedd4a 100644 --- 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 c7ecaf538..ef63730e2 100644 --- 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 f57d17641..301142f7f 100644 --- 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 aeeee5f55..a67c8ea93 100644 --- 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 55d159cd2..5317c5101 100644 --- 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 db9d00792..4905661fe 100644 --- 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 "" 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 "
\n"; KP.printf "Roles:\n" req; - KP.printf "%s\n" count + KP.printf "%s\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 "
" s; + KP.printf "
" s n k; KP.printf "⮞ " req_x; KP.printf "%s" req_s str in @@ -89,14 +95,16 @@ let status_out () = KP.printf "
\n" c; KP.printf "%s:\n" req str; KP.printf "%s\n" count; + filter p; KP.printf "
\n"; KP.printf "
\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 "\n" c s req str + KP.printf "\n" c s n k req str in let after_atoms () = KP.printf "
%s\ + %s
\n" diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webLWS.ml b/matita/matita/contribs/lambdadelta/bin/roles/webLWS.ml index 89dbfb5d2..35b658a1f 100644 --- 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 "" 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 "\n"; KP.printf "\n"; @@ -74,13 +74,15 @@ let open_out_html author description title css icon = KP.printf " \n"; KP.printf " \n"; KP.printf " \n"; + KP.printf " \n"; KP.printf " \n" author; KP.printf " \n" description; KP.printf " %s" title; - KP.printf " \n" css; KP.printf " \n" icon; + KP.printf " \n" css; KP.printf "\n"; - KP.printf "\n" + KP.printf "\n"; + KP.printf "