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