* Undo fixed.

* Minor code cleaning.

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index d4f7d5e008009da3a70f671ca15be7b707c3528f..49c3046b8eafeeaf74d0ccaa89635ac1df1289d4 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -131,7 +131,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         let b = 
           try
             let v = UM.strip_xpointer (UM.uri_of_string v) in
-            List.exists (fun (s,_) -> s = v) new_status.objects 
+            List.mem v new_status.objects 
           with UM.IllFormedUri _ -> false
         in
         if b then 

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 92999a49e3fd687869a76b499f7ceee45a5918a0..66e3528bf9da3351cfe1f7cd81c80e5c8085d391 100644 (file)
--- 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
-      *)

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 2d59ef95dea0c8d4df5b1aa469a9006ab8f98ead..dc692f8904cbd441273a27ec54f7d952f23b5189 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -71,7 +71,7 @@ type status = {
   moo_content_rev: moo;
   proof_status: proof_status;
   options: options;
-  objects: (UriManager.uri * string) list;
+  objects: UriManager.uri list;
   coercions: UriManager.uri list;
   notation_ids: CicNotation.notation_id list;
 }
@@ -108,8 +108,7 @@ let dump_status status =
   HLog.message "status.coercions\n";
   HLog.message "status.objects:\n";
   List.iter 
-    (fun (u,_) -> 
-      HLog.message (UriManager.string_of_uri u)) status.objects 
+    (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects 
   
 let get_option status name =
   try

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 321e26b99e9efcfdecae62346feb7fd3b3b1ad05..4fa2630ded20825b6eadbdd1a521b8def073757b 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -58,7 +58,7 @@ type status = {
   moo_content_rev: GrafiteMarshal.moo;
   proof_status: proof_status;                             (** logical status *)
   options: options;
-  objects: (UriManager.uri * string) list;  (** in-scope objects, with paths *)
+  objects: UriManager.uri list;  (** in-scope objects *)
   coercions: UriManager.uri list;                      (** defined coercions *)
   notation_ids: CicNotation.notation_id list;      (** in-scope notation ids *)
 }