fixed a finalization issue for connections closed twice

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 51007df29ea5a64a74986770a754bda14bb269b5..55cb4a45c09d45c887e07c26602934283bc61679 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -29,33 +29,34 @@ open MatitaTypes
 
 let alias_diff ~from status = 
   let module Map = DisambiguateTypes.Environment in
-  Map.fold
+  Map.fold_flatten
     (fun domain_item codomain_item acc ->
        if not (Map.mem domain_item from.aliases) then
-         Map.add domain_item codomain_item acc
+         Map.cons domain_item codomain_item acc
        else
          begin
            try 
-             let description1 = fst(Map.find domain_item from.aliases) in
-             let description2 = fst(Map.find domain_item status.aliases) in
-             if description1 <> description2 then
-               Map.add domain_item codomain_item acc
-             else
-               acc 
+             let codomain1 = Map.find domain_item from.aliases in
+             let codomain2 = Map.find domain_item status.aliases in
+             List.fold_right
+              (fun item env ->
+                let dsc = fst item in
+                if not (List.exists (fun (dsc', _) -> dsc'=dsc) codomain1) then
+                  Map.cons domain_item codomain_item env
+                else
+                  env)
+              codomain2 acc
            with Not_found -> acc
          end)
     status.aliases Map.empty
 
 let set_proof_aliases status aliases =
- let new_status = {status with aliases = aliases } in
+ let new_status = { status with aliases = aliases } in
  let diff = alias_diff ~from:status new_status 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}
+ if DisambiguateTypes.Environment.is_empty diff then
+   new_status
+ else
+   add_moo_content (DisambiguatePp.commands_of_environment diff) new_status
   
 (** given a uri and a type list (the contructors types) builds a list of pairs
  *  (name,uri) that is used to generate authomatic aliases **)
@@ -155,13 +156,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 =