X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Froles%2FwebEngine.ml;h=4e7bb32a834f5ff8e0e6ba4cc3c18fd59eba62cc;hb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea;hp=b5adc4ddd0ad2b3b64d28f8f149374fc38436073;hpb=cfccf434a57e10848d74d06674af4ec9cef0f0ca;p=helm.git
diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
index b5adc4ddd..4e7bb32a8 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
@@ -20,12 +20,13 @@ module WS = WebLWS
let error = ref ""
let open_out () =
- let author = "λδ development binary: roles manager" in
- let description = "λδ development binary: roles manager" in
- let title = "Roles Manager" in
- let css = Filename.concat !EG.base_url "css/roles.css" in
+ let author = "λδ development binary: role manager" in
+ let description = "λδ development binary: role manager" in
+ let title = "Role Manager" 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,12 @@ let string_of_request req arg =
WS.string_of_request "roles" (["system-"^req, arg], "")
let status_out () =
+ let filter p =
+ let req = string_of_request "select" p in
+ let ph = "Filter..." in
+ KP.printf "" ph req p p
+ in
let button_specs = [
"default", "Refresh";
"save", "Save";
@@ -42,28 +49,32 @@ let status_out () =
"remove", "Remove";
] in
let each_button (action, str) =
- let req = string_of_request action "" in
+ let req = string_of_request action "" in
KP.printf "%s\n" req str
in
let before_roles p count =
- let req = string_of_request "toggle" p in
+ let req = string_of_request "select" p in
KP.printf "
\n";
- KP.printf "Roles:\n" req;
- KP.printf "%s\n" count
+ KP.printf "Roles:\n" p req;
+ KP.printf "%s\n" count;
+ filter p
in
- let each_role p b str =
- let req = string_of_request "toggle" p in
+ let each_role n p b k o 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 n k o;
+ KP.printf "â® " req_x;
+ KP.printf "%s" req_s str
in
- let before_role p =
- KP.printf "
\n" p;
+ let before_role x n o =
+ let msg_n = if n then " (added)" else "" in
+ let msg_o = if o then " (removed)" else "" in
+ KP.printf "%s%s
\n" msg_n msg_o;
+ if x then KP.printf "
\n"
in
- let after_role () =
- KP.printf "
\n"
+ let after_role x =
+ if x then KP.printf "
\n"
in
let after_roles () =
KP.printf "
\n";
@@ -71,9 +82,10 @@ let status_out () =
List.iter each_button button_specs;
KP.printf "\n"
in
- let stage s =
+ let stage s m =
+ let msg_m = if m then " (modified)" else "" in
KP.printf "
\n"
in
let before_atoms a p count =
@@ -81,18 +93,20 @@ let status_out () =
if a then "object-color", "objects"
else "name-color", "names"
in
- let req = string_of_request "toggle" p in
+ let req = string_of_request "select" p in
KP.printf "
\n"
in
- let each_atom a p b str =
+ let each_atom a n p b k o 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 "toggle" p in
- KP.printf "