bugfix: evaluation of object commands is now atomic wrt status (including CicEnvironm...

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 707e31d988fff576c60795d8a257b6f1ec380179..79c6a4ddef6ca09fe64b7118009312724f269514 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -597,14 +597,19 @@ let eval_coercion status coercion =
   { status with proof_status = No_proof }
 
 let generate_elimination_principles uri status =
- let elim sort status =
-   try
-    let uri,obj = CicElim.elim_of ~sort uri 0 in
-     MatitaSync.add_obj uri obj status
-   with CicElim.Can_t_eliminate -> status
- in
- List.fold_left (fun status sort -> elim sort status) status
-  [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]
+  let status' = ref status in
+  let elim sort =
+    try
+      let uri,obj = CicElim.elim_of ~sort uri 0 in
+      status' := MatitaSync.add_obj uri obj !status'
+    with CicElim.Can_t_eliminate -> ()
+  in
+  try
+    List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+    !status'
+  with exn ->
+    MatitaSync.time_travel ~present:!status' ~past:status;
+    raise exn
 
 let generate_projections uri fields status =
  let projections = CicRecord.projections_of uri fields in
@@ -839,22 +844,29 @@ let eval_command opts status cmd =
           command_error (
             "metasenv not empty while giving a definition with body: " ^
             CicMetaSubst.ppmetasenv [] metasenv);
-         let status = MatitaSync.add_obj uri obj status in
-          match obj with
-             Cic.Constant _ -> status
+         let status' = ref status in
+         (try
+           status' := MatitaSync.add_obj uri obj !status';
+           (match obj with
+           | Cic.Constant _ -> ()
            | Cic.InductiveDefinition (_,_,_,attrs) ->
-              let status = generate_elimination_principles uri status in
-              let rec get_record_attrs =
-               function
-                  [] -> None
-                | (`Class (`Record fields))::_ -> Some fields
-                | _::tl -> get_record_attrs tl
-              in
+               status' := generate_elimination_principles uri !status';
+               let rec get_record_attrs =
+                 function
+                 | [] -> None
+                 | (`Class (`Record fields))::_ -> Some fields
+                 | _::tl -> get_record_attrs tl
+               in
                (match get_record_attrs attrs with
-                   None -> status (* not a record *)
-                 | Some fields -> generate_projections uri fields status)
+               | None -> () (* not a record *)
+               | Some fields ->
+                   status' := generate_projections uri fields !status')
            | Cic.CurrentProof _
-           | Cic.Variable _ -> assert false
+           | Cic.Variable _ -> assert false);
+           !status'
+         with exn ->
+           MatitaSync.time_travel ~present:!status' ~past:status;
+           raise exn)
 
 let eval_executable opts status ex =
   match ex with