X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Froles%2FwebEngine.ml;h=b5adc4ddd0ad2b3b64d28f8f149374fc38436073;hp=5dcc26e3618467a3ab543e7fa29ed2770f81be70;hb=cfccf434a57e10848d74d06674af4ec9cef0f0ca;hpb=7666f9dddfcaca5671dd25d3cd2095481968c7bf diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml index 5dcc26e36..b5adc4ddd 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml @@ -11,73 +11,117 @@ module KP = Printf -module EG = RolesGlobal module EE = RolesEngine +module EG = RolesGlobal +module ET = RolesTypes +module EU = RolesUtils +module WS = WebLWS -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 error = ref "" -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 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 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 "toggle" p in + KP.printf "
\n"; + KP.printf "Roles:\n" req; + KP.printf "%s\n" count + in + let each_role p b str = + let req = string_of_request "toggle" p in + let s = if b then " selected" else "" in + KP.printf "
" s; + KP.printf "⮞ " p; + KP.printf "%s" req str; + KP.printf "
\n" + in + let before_role p = + KP.printf "
\n" p; + in + let after_role () = + 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 = + KP.printf "
"; + KP.printf "Stage: %s" s; + KP.printf "
\n" + in let before_atoms a p count = let c, str = - if a then "object", "objects" - else "name", "names" + if a then "object-color", "objects" + else "name-color", "names" in + let req = string_of_request "toggle" p in KP.printf "
\n" c; - KP.printf "%s:\n" str; + KP.printf "%s:\n" req str; KP.printf "%s\n" count; KP.printf "
\n"; - KP.printf "
\n" + KP.printf "
\n" in let each_atom a p b str = - let c = if a then "object" else "name" in + let c = if a then "object-color" else "name-color" in let s = if b then " selected" else "" in - KP.printf "\n" c s str + let req = string_of_request "toggle" p in + KP.printf "\n" c s req str in let after_atoms () = KP.printf "
%s%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 + (before_atoms false) (each_atom false) after_atoms; + if !error <> "" then + KP.printf "
Error: %s
\n" !error -let init () = +let handler opt arg () = + begin try match opt with + | "system-default" -> () + | "system-add" -> EE.add_role () + | "system-remove" -> () + | "system-match" -> EE.add_matching () + | "system-toggle" -> EE.toggle_entry (EU.pointer_of_string arg) + | "system-save" -> EE.write_status () + | _ -> 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 (); status_out (); - close_out () + close_out (); + error := "" + +let init () = + WS.loop_in ignore handler ignore ()