From 08b2e9f42c841f03dade37e3c16d78e1bfdc946f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 3 Feb 2005 16:40:06 +0000
Subject: [PATCH] MetadataDb.clean doesn't need ~owner since table names are
 ownerized ;)

---
 helm/ocaml/metadata/metadataDb.ml  | 17 ++++++++++++++---
 helm/ocaml/metadata/metadataDb.mli |  2 +-
 2 files changed, 15 insertions(+), 4 deletions(-)

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 = 
diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index a1d7404bb..79bc82240 100644
--- 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
 
-- 
2.39.2