MetadataDb.clean doesn't need ~owner since table names are ownerized ;)

diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml
index 32aa329f3638224de482da81f6d476c38593e84e..c56a1a027d6fd900b7aa50c66fec3771cce5d14a 100644 (file)
--- 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 = 

diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index a1d7404bbe2acb7bb1a50282a640083dd3904891..79bc82240f329ec2a092610c00fb0ff5aca19a27 100644 (file)
--- a/helm/ocaml/metadata/metadataDb.mli
+++ b/helm/ocaml/metadata/metadataDb.mli
@@ -43,5 +43,5 @@ val index_inductive_def:
 (* TODO Zack indexing of variables and (perhaps?) incomplete proofs *)
 
   (** remove from the db all metadata pertaining to a given owner *)
-val clean: dbd:Mysql.dbd -> owner:string -> unit
+val clean: dbd:Mysql.dbd -> unit