let set_proof_aliases status aliases =
let new_status = {status with aliases = aliases } in
let diff = alias_diff ~from:status new_status in
- let moo_content_rev =
- DisambiguatePp.pp_environment diff ::
- status.moo_content_rev in
+ let textual_diff =
+ if DisambiguateTypes.Environment.is_empty diff then
+ ""
+ else
+ DisambiguatePp.pp_environment diff ^ "\n" in
+ let moo_content_rev = textual_diff :: status.moo_content_rev in
{new_status with moo_content_rev = moo_content_rev}
(** given a uri and a type list (the contructors types) builds a list of pairs
if CicEnvironment.in_library uri then
command_error (sprintf "%s already defined" suri)
else begin
- CicTypeChecker.typecheck_obj uri obj;
- MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
- let new_stuff = save_object_to_disk status uri obj in
- MatitaLog.message (sprintf "%s defined" suri);
- let status = add_aliases_for_object status suri obj in
- { status with objects = new_stuff @ status.objects;
- proof_status = No_proof }
+ CicTypeChecker.typecheck_obj uri obj; (* 1 *)
+ try
+ MetadataDb.index_obj ~dbd ~uri; (* 2 must be in the env *)
+ try
+ let new_stuff = save_object_to_disk status uri obj in (* 3 *)
+ try
+ MatitaLog.message (sprintf "%s defined" suri);
+ let status = add_aliases_for_object status suri obj in
+ { status with objects = new_stuff @ status.objects;
+ proof_status = No_proof }
+ with exc ->
+ List.iter MatitaMisc.safe_remove (List.map snd new_stuff); (* -3 *)
+ raise exc
+ with exc ->
+ ignore(MatitaDb.remove_uri uri); (* -2 *)
+ raise exc
+ with exc ->
+ CicEnvironment.remove_obj uri; (* -1 *)
+ raise exc
end
module OrderedUri =
MatitaMisc.safe_remove (Http_getter.resolve' uri)
with Http_getter_types.Key_not_found _ -> ());
remove_coercion uri;
- ignore (MatitaDb.remove_uri uri))
+ ignore (MatitaDb.remove_uri uri);
+ CicEnvironment.remove_obj uri)
to_remove