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=441302d0e065fa9a3da2d8d8d38676aca77570e9;hp=b5adc4ddd0ad2b3b64d28f8f149374fc38436073;hb=4d3256c98f816a2d2dc7b97557b61364e18d0806;hpb=cfccf434a57e10848d74d06674af4ec9cef0f0ca diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml index b5adc4ddd..441302d0e 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml @@ -46,21 +46,22 @@ let status_out () = 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 in let each_role p b str = - let req = string_of_request "toggle" p in + 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 "⮞ " p; - KP.printf "%s" req str; + KP.printf "⮞ " req_x; + KP.printf "%s" req_s str; KP.printf "
\n" in - let before_role p = - KP.printf "
\n" p; + let before_role () = + KP.printf "
\n"; in let after_role () = KP.printf "
\n" @@ -71,9 +72,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 "
"; - KP.printf "Stage: %s" s; + KP.printf "Stage: %s%s" s msg_m; KP.printf "
\n" in let before_atoms a p count = @@ -81,7 +83,7 @@ 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" c; KP.printf "%s:\n" req str; KP.printf "%s\n" count; @@ -91,7 +93,7 @@ let status_out () = 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 "toggle" p in + let req = string_of_request "select" p in KP.printf "%s\n" c s req str in let after_atoms () = @@ -109,10 +111,11 @@ let handler opt arg () = begin try match opt with | "system-default" -> () | "system-add" -> EE.add_role () - | "system-remove" -> () + | "system-remove" -> EE.remove_roles () | "system-match" -> EE.add_matching () - | "system-toggle" -> EE.toggle_entry (EU.pointer_of_string arg) + | "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