From: Stefano Zacchiroli Date: Tue, 27 Sep 2005 14:15:46 +0000 (+0000) Subject: moved list_uniq to the extlib X-Git-Tag: V_0_7_2_3~297 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0bf96cb668cdd8d14b1c66f8a5241f12c5df9e3a;p=helm.git moved list_uniq to the extlib --- diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml index 75d0f67e0..e3c7041dd 100644 --- a/helm/matita/matitaDb.ml +++ b/helm/matita/matitaDb.ml @@ -148,7 +148,7 @@ let remove_uri uri = let l = ref [] in HMysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l); let l = List.sort Pervasives.compare !l in - MatitaMisc.list_uniq l + HExtlib.list_uniq l with exn -> raise exn (* no errors should be accepted *) diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index e86e4b9a0..8f97b25a9 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -261,12 +261,6 @@ let obj_file_of_script f = let baseuri = baseuri_of_file f in obj_file_of_baseuri baseuri -let rec list_uniq = function - | [] -> [] - | h::[] -> [h] - | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) - | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl - let list_tl_at ?(equality=(==)) e l = let rec aux = function diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 0c2063095..1f72dbddd 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -56,8 +56,6 @@ val strip_trailing_slash: string -> string val normalize_dir: string -> string (** add trailing "/" if missing *) val strip_suffix: suffix:string -> string -> string -val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *) - (** @return tl tail of a list starting at a given element * @param eq equality to be used, defaults to physical equality (==) * @raise Not_found *) diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 51268acef..77a7d7b6f 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -62,7 +62,7 @@ let one_step_depend suri = l := uri :: !l | _ -> ()); let l = List.sort Pervasives.compare !l in - MatitaMisc.list_uniq l + HExtlib.list_uniq l with exn -> raise exn (* no errors should be accepted *) end @@ -77,7 +77,7 @@ let safe_buri_of_suri suri = let close_uri_list uri_to_remove = (* to remove an uri you have to remove the whole script *) let buri_to_remove = - MatitaMisc.list_uniq + HExtlib.list_uniq (List.fast_sort Pervasives.compare (List.map safe_buri_of_suri uri_to_remove)) in @@ -117,8 +117,7 @@ let close_uri_list uri_to_remove = (fun acc u -> one_step_depend u @ acc) [] uri_to_remove in let depend = - MatitaMisc.list_uniq - (List.fast_sort Pervasives.compare depend) + HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) in uri_to_remove, depend @@ -136,7 +135,7 @@ let clean_baseuris ?(verbose=true) buris = if debug then List.iter debug_prerr buris; let l = close [] buris in - let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in + let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in let l = List.map UriManager.uri_of_string l in debug_prerr "clean_baseuri will remove:"; if debug then diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 5a73c099b..40f91235a 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -107,7 +107,7 @@ let main () = (fun file -> let deps = Hashtbl.find_all include_deps file in let deps = List.fast_sort Pervasives.compare deps in - let deps = MatitaMisc.list_uniq deps in + let deps = HExtlib.list_uniq deps in let deps = file :: deps in let moo = MatitaMisc.obj_file_of_script file in Printf.printf "%s: %s\n" moo (String.concat " " deps);