X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Froles%2FwebEngine.ml;h=db9d007923edee60d73781dc3b17c1c984ffd80d;hb=456a157eba1428fd4ec02713e60ac2b653a0e0b0;hp=7fc9429605ca57c97f75b3a2fe5c9547ca7688a5;hpb=2c9f4fddc259b09b6e71b18eef78f0bed38eeb14;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml index 7fc942960..db9d00792 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml @@ -11,48 +11,122 @@ module KP = Printf -module EG = RolesGlobal module EE = RolesEngine +module EG = RolesGlobal +module ET = RolesTypes +module EU = RolesUtils +module WS = WebLWS + +let error = ref "" -let open_out_html author description title css icon = -(* - YW.open_out "application/xhtml+xml" 0; -*) - KP.printf "\n"; - KP.printf "\n"; - KP.printf "\n"; - KP.printf "\n"; - KP.printf " \n"; - KP.printf " \n"; - 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"; - KP.printf "\n" - -let close_out_html () = - KP.printf "\n"; - KP.printf "\n" -(* - YW.close_out () -*) let open_out () = - let author = "λδ development binary: roles manager" in - let description = "λδ development binary: roles manager" in - let title = "Roles Manager" in + 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 - open_out_html author description title css icon + WS.open_out_html author description title css icon let close_out () = - close_out_html () + WS.close_out_html () -let init () = +let string_of_request req arg = + WS.string_of_request "roles" (["system-"^req, arg], "") + +let status_out () = + let button_specs = [ + "default", "Refresh"; + "save", "Save"; + "add", "Add"; + "match", "Match"; + "remove", "Remove"; + ] in + let each_button (action, str) = + let req = string_of_request action "" in + KP.printf "%s\n" req str + in + let before_roles p count = + let req = string_of_request "select" p in + KP.printf "
\n"; + KP.printf "Roles:\n" req; + KP.printf "%s\n" count + in + let each_role p b 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 "⮞ " req_x; + KP.printf "%s" req_s str + in + 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 x = + if x then KP.printf "
\n" + in + let after_roles () = + KP.printf "
\n"; + KP.printf "
\n"; + List.iter each_button button_specs; + KP.printf "
\n" + in + let stage s m = + let msg_m = if m then " (modified)" else "" in + KP.printf "
"; + KP.printf "Stage: %s%s" s msg_m; + KP.printf "
\n" + in + let before_atoms a p count = + let c, str = + if a then "object-color", "objects" + else "name-color", "names" + in + let req = string_of_request "select" p in + KP.printf "
\n" c; + KP.printf "%s:\n" req str; + KP.printf "%s\n" count; + KP.printf "
\n"; + KP.printf "
\n" + in + let each_atom a p b 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 + in + let after_atoms () = + KP.printf "
%s
\n" + in + KP.printf "
Role Manager
\n"; + EE.visit_status + before_roles each_role before_role after_role after_roles stage + (before_atoms true) (each_atom true) after_atoms + (before_atoms false) (each_atom false) after_atoms; + if !error <> "" then + KP.printf "
Error: %s
\n" !error + +let handler opt arg () = + begin try match opt with + | "system-default" -> () + | "system-add" -> EE.add_role () + | "system-remove" -> EE.remove_roles () + | "system-match" -> EE.add_matching () + | "system-select" -> EE.select_entry (EU.pointer_of_string arg) + | "system-save" -> EE.write_status () + | "system-expand" -> EE.expand_entry (EU.pointer_of_string arg) + | _ -> EU.raise_error (ET.EWrongRequest (opt, arg)) + with + | ET.Error e -> error := EU.string_of_error e + | e -> error := Printexc.to_string e + end; open_out (); - close_out () + status_out (); + close_out (); + error := "" + +let init () = + WS.loop_in ignore handler ignore ()