]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/library/libraryClean.ml
Porting to ocaml 5
[helm.git] / matita / components / library / libraryClean.ml
index 6f58bb54eaadb79274c1cca29328b1a7b4aaab0f..ebd02bd1bc4f9e5e1352b24f73acc45e08e13224 100644 (file)
 
 (* $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 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,18 +217,19 @@ 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 = 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
@@ -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
+   (HExtlib.list_uniq (List.fast_sort Stdlib.compare
      (List.map NUri.baseuri_of_uri l @ buris)))
+*)