From: Ferruccio Guidi Date: Fri, 7 Feb 2020 12:44:42 +0000 (+0100) Subject: update in binaries for λδ X-Git-Tag: make_still_working~192 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3be6630ba2a592488502b320e85e45b55a099580 update in binaries for λδ roles: more transient information in the status roles: refactored options -o -s -t to -t -n -s --- diff --git a/matita/matita/contribs/lambdadelta/bin/roles/roles.ml b/matita/matita/contribs/lambdadelta/bin/roles/roles.ml index 6d9620c8f..bcb66d864 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/roles.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/roles.ml @@ -22,13 +22,13 @@ let help_W = " Run as an LWS application" let help_X = " Reset all options to defaults" let help_a = " Add selected names to a role" let help_m = " Add roles relating matching names" -let help_o = " Add top objects for this stage" +let help_n = " Start a stage with this version" let help_p = " Print current status on standard output" let help_r = " Load current status" -let help_s = " Start a stage with this version" -let help_t = " Toggle the selection of this pointed entry" +let help_s = " Toggle the selection of this pointed entry" +let help_t = " Add top objects for this stage" let help_w = " Save current status" -let help = "Usage: roles [ -LWXamprw | -B | -C | -os | -t | ]*" +let help = "Usage: roles [ -LWXamprw | -B | -C | -nt | -s | ]*" let change_cwd s = EG.cwd := Filename.concat !EG.cwd s @@ -39,8 +39,8 @@ let add_tops s = let new_stage s = EE.new_stage (EU.version_of_string s) -let toggle_entry s = - EE.toggle_entry (EU.pointer_of_string s) +let select_entry s = + EE.select_entry (EU.pointer_of_string s) let process s = match Filename.extension s with @@ -56,11 +56,11 @@ let _main = try "-X", Arg.Unit EG.clear, help_X; "-a", Arg.Unit EE.add_role, help_a; "-m", Arg.Unit EE.add_matching, help_m; - "-o", Arg.String add_tops, help_o; + "-n", Arg.String new_stage, help_n; "-p", Arg.Unit EE.print_status, help_p; "-r", Arg.Unit EE.read_status, help_r; - "-s", Arg.String new_stage, help_s; - "-t", Arg.String toggle_entry, help_t; + "-s", Arg.String select_entry, help_s; + "-t", Arg.String add_tops, help_t; "-w", Arg.Unit EE.write_status, help_w; ] process help with ET.Error e -> Printf.eprintf "roles: %s\n%!" (EU.string_of_error e) diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml index 6af2b3fbd..ce6f403ea 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml @@ -18,10 +18,13 @@ module ET = RolesTypes let st = EU.new_status let new_stage v = - if st.ET.w = [] then st.ET.s <- v - else EU.raise_error ET.EWaiting + if st.ET.w = [] then begin + if EU.compare_versions st.ET.s v <> 0 then begin + st.ET.s <- v; st.ET.m <- true + end + end else EU.raise_error ET.EWaiting -let toggle_entry = function +let select_entry = function | [0] -> st.ET.r <- EU.list_toggle_all st.ET.r | [0;m] -> st.ET.r <- EU.list_toggle m st.ET.r | [0;m;1] -> @@ -48,31 +51,32 @@ let add_role () = if os = [] && ns = [] then () else begin match EU.list_select None st.ET.r with | None -> - let r = {ET.v = st.ET.s; ET.o = os; ET.n = ns} in + let r = {ET.x = false; ET.v = st.ET.s; ET.o = os; ET.n = ns} in st.ET.r <- EU.roles_union [false, r] st.ET.r | Some r -> if r.ET.v <> st.ET.s then EU.raise_error ET.EWrongVersion else r.ET.o <- EU.objs_union os r.ET.o; r.ET.n <- EU.names_union ns r.ET.n; end; - st.ET.t <- ts; st.ET.w <- ws + st.ET.t <- ts; st.ET.w <- ws; st.ET.m <- true let add_tops v = if EU.exists_role_deleted st.ET.s st.ET.r || st.ET.t <> [] then EU.raise_error ET.ETops else let ds, ts = EU.get_tops v st.ET.r in if ds <> [] then begin - let r = {ET.v = st.ET.s; ET.o = ds; ET.n = []} in + let r = {ET.x = false; ET.v = st.ET.s; ET.o = ds; ET.n = []} in st.ET.r <- EU.roles_union [false, r] st.ET.r end; - if ts <> [] then st.ET.t <- ts + if ts <> [] then st.ET.t <- ts; + if ds <> [] || ts <> [] then st.ET.m <- true let rec add_matching () = match EU.match_names 0 0 st.ET.t st.ET.w with | None -> () | Some (ti,wi) -> - toggle_entry [1;ti]; - toggle_entry [2;wi]; + select_entry [1;ti]; + select_entry [2;wi]; add_role (); add_matching () @@ -82,7 +86,8 @@ let read_waiting fname = let ws = EI.read_rev_names ich [] in Scanf.Scanning.close_in ich; let map ws w = EU.names_union ws [w] in - st.ET.w <- List.fold_left map st.ET.w ws + st.ET.w <- List.fold_left map st.ET.w ws; + if ws <> [] then st.ET.m <- true let read_status () = if st.ET.s <> [] then EU.raise_error (ET.EStage st.ET.s) else @@ -90,6 +95,7 @@ let read_status () = let ich = open_in fname in let tmp = EI.read_status ich in close_in ich; + st.ET.m <- tmp.ET.m; st.ET.r <- tmp.ET.r; st.ET.s <- tmp.ET.s; st.ET.t <- tmp.ET.t; @@ -99,7 +105,8 @@ let write_status () = let fname = Filename.concat !EG.cwd "roles.osn" in let och = open_out fname in EO.out_status och st; - close_out och + close_out och; + st.ET.m <- false let print_status () = EO.out_status stdout st @@ -109,12 +116,14 @@ let visit_status before_t each_t after_t before_w each_w after_w = let visit_tw _ _ = () in let visit_r p r = - before (EU.string_of_pointer (List.rev p)); - EU.list_visit before_t each_t visit_tw after_t EU.string_of_obj (1::p) r.ET.o; - EU.list_visit before_w each_w visit_tw after_w EU.string_of_name (2::p) r.ET.n; - after () + if r.ET.x then begin + before (); + EU.list_visit before_t each_t visit_tw after_t EU.string_of_obj (1::p) r.ET.o; + EU.list_visit before_w each_w visit_tw after_w EU.string_of_name (2::p) r.ET.n; + after () + end in EU.list_visit before_r each_r visit_r after_r EU.string_of_role [0] st.ET.r; - stage (EU.string_of_version st.ET.s); + stage (EU.string_of_version st.ET.s) st.ET.m; EU.list_visit before_t each_t visit_tw after_t EU.string_of_obj [1] st.ET.t; EU.list_visit before_w each_w visit_tw after_w EU.string_of_name [2] st.ET.w diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli index 0f5c9c16f..828e52994 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli +++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli @@ -11,7 +11,7 @@ val new_stage: RolesTypes.version -> unit -val toggle_entry: RolesTypes.pointer -> unit +val select_entry: RolesTypes.pointer -> unit val add_role: unit -> unit @@ -29,7 +29,7 @@ val print_status: unit -> unit val visit_status: (string -> string -> unit) -> (string -> bool -> string -> unit) -> - (string -> unit) -> (unit -> unit) -> (unit -> unit) -> (string -> unit) -> + (unit -> unit) -> (unit -> unit) -> (unit -> unit) -> (string -> bool -> unit) -> (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) -> (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) -> unit diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesParser.mly b/matita/matita/contribs/lambdadelta/bin/roles/rolesParser.mly index 990ca672e..f901e4492 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/rolesParser.mly +++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesParser.mly @@ -36,7 +36,7 @@ name: role: | OP REL ver olds news CP { - false, {ET.v = $3; ET.o = $4; ET.n = $5} + false, {ET.x = false; ET.v = $3; ET.o = $4; ET.n = $5} } ; @@ -73,6 +73,6 @@ base: status: | ROLES SC OP TOP base ver olds news CP EOF { - {ET.r = $5; ET.s = $6; ET.t = $7; ET.w = $8} + {ET.m = false; ET.r = $5; ET.s = $6; ET.t = $7; ET.w = $8} } ; diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesTypes.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesTypes.ml index 1535c493b..f02af7021 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/rolesTypes.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesTypes.ml @@ -20,6 +20,7 @@ type obj = version * name type objs = (bool*obj) list type role = { + mutable x: bool; mutable v: version; mutable o: objs; mutable n: names; @@ -28,6 +29,7 @@ type role = { type roles = (bool*role) list type status = { + mutable m: bool; mutable r: roles; mutable s: version; mutable t: objs; diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml index 5fdf312f7..c4b60552c 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml @@ -164,7 +164,7 @@ let rec match_names oi ni os ns = Some (oi, ni) let new_status = { - ET.r = []; ET.s = []; ET.t = []; ET.w = []; + ET.m = false; ET.r = []; ET.s = []; ET.t = []; ET.w = []; } let string_of_pointer = string_of_version diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli index 526629295..92acc162a 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli +++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli @@ -30,6 +30,8 @@ val string_of_version: RolesTypes.version -> string val version_of_string: string -> RolesTypes.version +val compare_versions: RolesTypes.version -> RolesTypes.version -> int + val string_of_name: RolesTypes.name -> string val name_of_string: string -> RolesTypes.name diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml index b5adc4ddd..9fc545b3e 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml @@ -46,21 +46,21 @@ 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 = 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 "
\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 +71,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 +82,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 +92,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 () = @@ -111,7 +112,7 @@ let handler opt arg () = | "system-add" -> EE.add_role () | "system-remove" -> () | "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 () | _ -> EU.raise_error (ET.EWrongRequest (opt, arg)) with