X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;fp=helm%2Fmatita%2FmatitaSync.ml;h=66e3528bf9da3351cfe1f7cd81c80e5c8085d391;hb=c307d27343fe48aeeb2e1763a811f8122ac1c0df;hp=92999a49e3fd687869a76b499f7ceee45a5918a0;hpb=019d5023aefd04aff9ac0849405306612d54ba64;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 92999a49e..66e3528bf 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -117,6 +117,7 @@ let add_aliases_for_object status uri =
 let add_obj uri obj status =
  let basedir = Helm_registry.get "matita.basedir" in
  let lemmas = LibrarySync.add_obj uri obj basedir in
+ let status = {status with objects = uri::status.objects} in
   List.fold_left add_alias_for_constant
    (add_aliases_for_object status uri obj) lemmas
 
@@ -140,13 +141,6 @@ module UriSet = Set.Make (OrderedUri)
 module IdSet  = Set.Make (OrderedId)
 
   (** @return l2 \ l1 *)
-let urixstring_list_diff l2 l1 =
-  let module S = UriSet in
-  let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
-  let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
-  let diff = S.diff s2 s1 in
-  S.fold (fun uri uris -> uri :: uris) diff []
-
 let uri_list_diff l2 l1 =
   let module S = UriManager.UriSet in
   let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
@@ -163,7 +157,7 @@ let id_list_diff l2 l1 =
   S.fold (fun uri uris -> uri :: uris) diff []
 
 let time_travel ~present ~past =
-  let objs_to_remove = urixstring_list_diff present.objects past.objects in
+  let objs_to_remove = uri_list_diff present.objects past.objects in
   let coercions_to_remove = uri_list_diff present.coercions past.coercions in
   let notation_to_remove =
     id_list_diff present.notation_ids past.notation_ids
@@ -172,43 +166,5 @@ let time_travel ~present ~past =
   List.iter
    (fun uri -> CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri))
    coercions_to_remove;
-  List.iter
-    (fun (uri,p) -> 
-      HExtlib.safe_remove p;
-      (try 
-        CicEnvironment.remove_obj uri
-      with CicEnvironment.Object_not_found _ -> 
-        HLog.debug
-          (sprintf "time_travel removes from cache %s that is not in" 
-            (UriManager.string_of_uri uri)));
-      let l = LibraryDb.remove_uri uri in
-      debug_list := UriManager.string_of_uri uri :: !debug_list @ l) 
-    objs_to_remove;
+  List.iter LibrarySync.remove_obj objs_to_remove;
   List.iter CicNotation.remove_notation notation_to_remove
-  (*
-  (* this is debug code
-  * idea: debug_list is the list of objects to be removed as computed from the
-  * db, while list_of_objs_to_remove is the same list but computer from the
-  * differences between statuses *)
-  let l1 = List.sort Pervasives.compare !debug_list in
-  let l2 = List.sort Pervasives.compare 
-    (List.map (fun (x,_) -> UriManager.string_of_uri x) list_of_objs_to_remove)
-  in
-  let rec uniq = function 
-    | [] -> []
-    | h::[] -> [h]
-    | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl)
-    | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl
-  in
-  let l1 =  uniq l1 in
-  let l2 =  uniq l2 in
-  try
-    List.iter2 (fun x y -> if x <> y then raise Exit) l1 l2
-  with
-  | Invalid_argument _ | Exit -> 
-      HLog.debug "It seems you garbaged something...";
-      HLog.debug "l1:";
-      List.iter HLog.debug l1;
-      HLog.debug "l2:";
-      List.iter HLog.debug l2
-      *)