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 6d9620c8f633451fe3caffca93bf105161ea849c..bcb66d86481d699042a0f2ff076c7ac0b887b825 100644 (file)
--- 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 = "<version>  Add top objects for this stage"
+let help_n = "<version>  Start a stage with this version"
 let help_p = " Print current status on standard output"
 let help_r = " Load current status"
-let help_s = "<version>  Start a stage with this version"
-let help_t = "<pointer>  Toggle the selection of this pointed entry"
+let help_s = "<pointer>  Toggle the selection of this pointed entry"
+let help_t = "<version>  Add top objects for this stage"
 let help_w = " Save current status"
-let help   = "Usage: roles [ -LWXamprw | -B <url> | -C <dir> | -os <version> | -t <pointer> | <file> ]*"
+let help   = "Usage: roles [ -LWXamprw | -B <url> | -C <dir> | -nt <version> | -s <pointer> | <file> ]*"
 
 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 6af2b3fbd1b5adecc4dc5bd257c54cf7a9728887..ce6f403ea1f2b9060b57203d8c40b588b35839e8 100644 (file)
--- 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 0f5c9c16f83afd0049d5953630038d9386306937..828e529946ef38ce08565a71642b944abe12122e 100644 (file)
--- 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 990ca672ecaa352a35278cbbff726c890adec944..f901e44926b6f4ea77e90c4f9864fb1a4aae030a 100644 (file)
--- 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 1535c493be77a484e42547a93fa4c0e62a055cc7..f02af702181744c001b75bd2f95b3c070a72f231 100644 (file)
--- 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 5fdf312f70321584b0e78b59c95babce4ed7e09f..c4b60552c941cf3a4216d7ebf056daacce8292bb 100644 (file)
--- 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 5266292950086ab062f40e3e769528e8d96630e0..92acc162a432bf261733c28539173db753e9e796 100644 (file)
--- 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 b5adc4ddd0ad2b3b64d28f8f149374fc38436073..9fc545b3e3031e1d6590535ce349820ee5485756 100644 (file)
--- 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 "<span class=\"button\"><a href=\"%s\">%s</a></span>\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 "<div class=\"roles-head role-color\">\n";
     KP.printf "<a href=\"%s\">Roles:</a>\n" req;
     KP.printf "<span class=\"count\">%s</span>\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 "<div class=\"role role-color%s\">" s;
     KP.printf "<a href=\"#%s\">⮞</a> " p;
     KP.printf "<a href=\"%s\">%s</a>" req str;
     KP.printf "</div>\n"
   in
-  let before_role p =
-    KP.printf "<div id=\"%s\" class=\"roles\">\n" p;
+  let before_role () =
+    KP.printf "<div class=\"roles\">\n";
   in
   let after_role () =
     KP.printf "</div>\n"
@@ -71,9 +71,10 @@ let status_out () =
     List.iter each_button button_specs;
     KP.printf "</div>\n"
   in
-  let stage s =
+  let stage s m =
+    let msg_m = if m then " (modified)" else "" in
     KP.printf "<div class=\"stage role-color\">";
-    KP.printf "Stage: %s" s;
+    KP.printf "Stage: %s%s" s msg_m;
     KP.printf "</div>\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 "<div class=\"atoms-head %s\">\n" c;
     KP.printf "<a href=\"%s\">%s:</a>\n" req str;
     KP.printf "<span class=\"count\">%s</span>\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 "<td class=\"atom %s%s\"><a href=\"%s\">%s</a></td>\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