X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fmetadata%2FmetadataDb.ml;h=c56a1a027d6fd900b7aa50c66fec3771cce5d14a;hb=e097097df79962ad19cc1c4b75e8814b41fa1c64;hp=32aa329f3638224de482da81f6d476c38593e84e;hpb=12cb072c7bbb5119f4328f637add61ae2228b8c7;p=helm.git

diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml
index 32aa329f3..c56a1a027 100644
--- a/helm/ocaml/metadata/metadataDb.ml
+++ b/helm/ocaml/metadata/metadataDb.ml
@@ -113,7 +113,7 @@ let index_inductive_def ~dbd =
     List.iter (insert_const_no dbd) uris;
     List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
 
-let clean ~(dbd:Mysql.dbd) ~owner =
+let clean ~(dbd:Mysql.dbd) =
   let owned_uris =  (* list of uris in list-of-columns format *)
     let query =
       (* sprintf 
@@ -122,10 +122,21 @@ let clean ~(dbd:Mysql.dbd) ~owner =
       sprintf "SELECT source FROM %s" (obj_tbl ())
     in
     let result = Mysql.exec dbd query in
-    Mysql.map result (fun cols ->
+    let uris = Mysql.map result (fun cols ->
       match cols.(0) with
       | Some src -> src
-      | None -> assert false)
+      | None -> assert false) in
+    (* and now some stuff to remove #xpointers and duplicates *)
+    let cleaned_uris = 
+      List.map (fun x -> Str.replace_first (Str.regexp "\#.*$") "" x) uris
+    in
+    let sorted_uris = List.fast_sort Pervasives.compare cleaned_uris in
+    match sorted_uris with
+    | [] -> sorted_uris
+    | he::tl -> 
+        (* no List.remove dups ?? *)
+        snd(List.fold_left (fun (last,l) cur -> if cur <> last then
+        (cur,cur::l) else (last,l)) (he,[he]) tl)
   in
   let del_from tbl =
     let query s =