]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataDb.ml
MetadataDb.clean doesn't need ~owner since table names are ownerized ;)
[helm.git] / helm / ocaml / metadata / metadataDb.ml
index 32aa329f3638224de482da81f6d476c38593e84e..c56a1a027d6fd900b7aa50c66fec3771cce5d14a 100644 (file)
@@ -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 =