X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=e12c1cd146c11506322c8c19514c8d6e1bb9209e;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=4df2ab7fbec0a41d0973feebf1cbed0cfb0cc658;hpb=6b5e1d495c61f459738187e8d71efadb162abdbe;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 4df2ab7fb..e12c1cd14 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -49,9 +49,12 @@ let alias_diff ~from status =
 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
@@ -152,13 +155,25 @@ let add_obj uri obj status =
   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 =
@@ -263,5 +278,6 @@ let remove ~verbose uri =
         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