X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flibrary%2FlibraryClean.ml;h=ebd02bd1bc4f9e5e1352b24f73acc45e08e13224;hb=3d2976d83978e59e411800dac69124af5a0a8ef7;hp=1f92b5868d7102aa13e152aac3cbbc49fa211034;hpb=cd5e575ed60527edac0a99196bd8d20f06841254;p=helm.git diff --git a/matita/components/library/libraryClean.ml b/matita/components/library/libraryClean.ml index 1f92b5868..ebd02bd1b 100644 --- a/matita/components/library/libraryClean.ml +++ b/matita/components/library/libraryClean.ml @@ -25,16 +25,14 @@ (* $Id$ *) -open Printf - let debug = false let debug_prerr = if debug then prerr_endline else ignore -module HGT = Http_getter_types;; -module HG = Http_getter;; -module UM = UriManager;; +(*module HGT = Http_getter_types;;*) +(*module HG = Http_getter;;*) +(*module UM = UriManager;;*) -let decompile = ref (fun ~baseuri -> assert false);; +let decompile = ref (fun ~baseuri:_ -> assert false);; let set_decompile_cb f = decompile := f;; (* @@ -87,7 +85,7 @@ let one_step_depend cache_of_processed_baseuri suri dbtype dbd = Filename.dirname (strip_xpointer occ) = buri -> l := uri :: !l | _ -> ()); - let l = List.sort Pervasives.compare !l in + let l = List.sort Stdlib.compare !l in HExtlib.list_uniq l with exn -> raise exn (* no errors should be accepted *) @@ -122,7 +120,7 @@ let db_uris_of_baseuri buri = | Some uri when Filename.dirname (strip_xpointer uri) = buri -> l := uri :: !l | _ -> ()); - let l = List.sort Pervasives.compare !l in + let l = List.sort Stdlib.compare !l in HExtlib.list_uniq l with exn -> raise exn (* no errors should be accepted *) @@ -137,7 +135,7 @@ let close_uri_list cache_of_processed_baseuri uri_to_remove = (* to remove an uri you have to remove the whole script *) let buri_to_remove = HExtlib.list_uniq - (List.fast_sort Pervasives.compare + (List.fast_sort Stdlib.compare (List.map safe_buri_of_suri uri_to_remove)) in (* cleand the already visided baseuris *) @@ -179,7 +177,7 @@ let close_uri_list cache_of_processed_baseuri uri_to_remove = in let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in let uri_to_remove = - HExtlib.list_uniq (List.sort Pervasives.compare uri_to_remove) in + HExtlib.list_uniq (List.sort Stdlib.compare uri_to_remove) in (* now we want the list of all uri that depend on them *) let depend = List.fold_left @@ -187,7 +185,7 @@ let close_uri_list cache_of_processed_baseuri uri_to_remove = [] uri_to_remove in let depend = - HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) + HExtlib.list_uniq (List.fast_sort Stdlib.compare depend) in uri_to_remove, depend ;; @@ -219,22 +217,23 @@ let moo_root_dir = lazy ( ;; *) -let rec close_db cache_of_processed_baseuri uris next = - prerr_endline "CLOSE_DB "; uris (* MATITA 1.0 *) +let close_db _cache_of_processed_baseuri uris _next = + uris (* MATITA 1.0 *) ;; -let clean_baseuris ?(verbose=true) buris = +let clean_baseuris ?verbose:(_=true) _buris = + (* MATITA 1.0 *) () (* let cache_of_processed_baseuri = Hashtbl.create 1024 in let buris = List.map Http_getter_misc.strip_trailing_slash buris in debug_prerr "clean_baseuris called on:"; if debug then List.iter debug_prerr buris; let l = close_db cache_of_processed_baseuri [] buris in - let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in - let l = List.map UriManager.uri_of_string l in + let l = HExtlib.list_uniq (List.fast_sort Stdlib.compare l) in + let l = List.map NUri.uri_of_string l in debug_prerr "clean_baseuri will remove:"; if debug then - List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; + List.iter (fun u -> debug_prerr (NUri.string_of_uri u)) l; List.iter (fun baseuri -> !decompile ~baseuri; @@ -246,5 +245,6 @@ let clean_baseuris ?(verbose=true) buris = HExtlib.safe_remove lexiconfile; HExtlib.rmdir_descend (Filename.chop_extension lexiconfile) with Http_getter_types.Key_not_found _ -> ()) - (HExtlib.list_uniq (List.fast_sort Pervasives.compare - (List.map (UriManager.buri_of_uri) l @ buris))) + (HExtlib.list_uniq (List.fast_sort Stdlib.compare + (List.map NUri.baseuri_of_uri l @ buris))) +*)