X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=9c6c53aeef5e2d43465b98e524c21aecb67112ef;hb=6beda5aa100b617b75d88a5a519b5022c99208a0;hp=c6682bd9100df786a88c71425230f8a219de07ed;hpb=92365dd290f8916cc2f6b09011134ffadf97f3ed;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index c6682bd91..9c6c53aee 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -169,7 +169,8 @@ let add_single_obj uri obj refinement_toolkit =
         (* EXPERIMENTAL: pretty print the object in natural language *)
 	(try !object_declaration_hook uri obj
 	 with exc ->
-	  prerr_endline "Error: object_declaration_hook failed");
+	  prerr_endline ("Error: object_declaration_hook failed"^
+          Printexc.to_string exc));
         try 
          HLog.message
           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
@@ -243,6 +244,29 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,_,_) -> true)
 
+let stack = ref [];;
+
+let h2l h =
+  UriManager.UriHashtbl.fold 
+  (fun k v acc -> (k,v) :: acc) h []
+;;
+
+let push () =
+  stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack;
+  remove_all_coercions ()
+;;
+
+let pop () =
+  match !stack with
+  | [] -> raise (Failure "Unable to POP from librarySync.ml")
+  | (db,h) :: tl -> 
+      stack := tl;
+      remove_all_coercions ();
+      CoercDb.restore db;
+      List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v)
+      h
+;;
+
 let add_coercion ~add_composites refinement_toolkit uri arity saturations
  baseuri
 =
@@ -318,7 +342,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
       (CoercDb.to_list ())
   in
   if not add_composites then
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+    UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
+    [])
   else
     let new_coercions = 
       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
@@ -337,14 +363,11 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
     (* add the composites obj and they eventual lemmas *)
     let lemmas = 
-      if add_composites then
         List.fold_left
           (fun acc (_,tgt,uri,saturations,obj,arity) -> 
             add_single_obj uri obj refinement_toolkit;
              (uri,arity,saturations)::acc) 
           [] new_coercions
-      else
-        []
     in
     (* store that composite_uris are related to uri. the first component is
      * the stuff in the DB while the second is stuff for remove_obj *)
@@ -354,8 +377,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
        List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
         composite_uris; 
     *)
-    UriManager.UriHashtbl.add coercion_hashtbl uri 
-      (composite_uris,if add_composites then composite_uris else []);
+    UriManager.UriHashtbl.add 
+      coercion_hashtbl uri (composite_uris,composite_uris);
     (*
     prerr_endline ("lemmas:");
       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
@@ -373,7 +396,8 @@ let remove_coercion uri =
     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
       composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
-    CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u);
+    CoercDb.remove_coercion 
+      (fun (_,_,u,_) -> UriManager.eq uri u);
     (* remove from the DB *) 
     List.iter 
       (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
@@ -381,7 +405,7 @@ let remove_coercion uri =
     (* remove composites from the lib *)
     List.iter remove_single_obj composites_in_lib
   with
-    Not_found -> () (* mhh..... *)
+    Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
     
 
 let generate_projections refinement_toolkit uri fields =