From c307d27343fe48aeeb2e1763a811f8122ac1c0df Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Nov 2005 11:59:27 +0000 Subject: [PATCH] * Undo fixed. * Minor code cleaning. --- helm/matita/matitaScript.ml | 2 +- helm/matita/matitaSync.ml | 50 +++---------------------------------- helm/matita/matitaTypes.ml | 5 ++-- helm/matita/matitaTypes.mli | 2 +- 4 files changed, 7 insertions(+), 52 deletions(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index d4f7d5e00..49c3046b8 100644 --- 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 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 - *) diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 2d59ef95d..dc692f890 100644 --- 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 321e26b99..4fa2630de 100644 --- 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 *) } -- 2.39.2