X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataDb.ml;h=4b7664c224fdac212b9e5700b0fa800c74de4c73;hb=0aaed6f96b856d1181a3cd1f2ef3ea4a91990771;hp=c56a1a027d6fd900b7aa50c66fec3771cce5d14a;hpb=08b2e9f42c841f03dade37e3c16d78e1bfdc946f;p=helm.git

diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml
index c56a1a027..4b7664c22 100644
--- a/helm/ocaml/metadata/metadataDb.ml
+++ b/helm/ocaml/metadata/metadataDb.ml
@@ -45,7 +45,7 @@ let prepare_insert () =
   ((*insert_owner, *)insert_sort, insert_rel, insert_obj)
 
 let execute_insert dbd ((*insert_owner, *)insert_sort, insert_rel, insert_obj)
-  uri owner (sort_cols, rel_cols, obj_cols)
+  uri (sort_cols, rel_cols, obj_cols)
 =
   (* ignore (Mysql.exec dbd (insert_owner uri owner)); *)
   List.iter (function
@@ -90,53 +90,49 @@ let insert_name ~dbd ~uri ~name =
 type columns =
   MetadataPp.t list list * MetadataPp.t list list * MetadataPp.t list list
 
+  (* TODO ZACK: verify if an object has already been indexed *)
+let already_indexed _ = false
+
 let index_constant ~dbd =
   let query = prepare_insert () in
-  fun ~owner ~uri ~body ~ty  ->
-    let name = UriManager.name_of_uri uri in
-    let uri = UriManager.string_of_uri uri in
-    let metadata = MetadataExtractor.compute ~body ~ty in
-    let columns = MetadataPp.columns_of_metadata ~about:uri metadata in
-    execute_insert dbd query uri owner (columns :> columns);
-    insert_const_no dbd uri;
-    insert_name ~dbd ~uri ~name
+  fun ~uri ~body ~ty  ->
+    if not (already_indexed uri) then begin
+      let name = UriManager.name_of_uri uri in
+      let uri = UriManager.string_of_uri uri in
+      let metadata = MetadataExtractor.compute ~body ~ty in
+      let columns = MetadataPp.columns_of_metadata ~about:uri metadata in
+      execute_insert dbd query uri (columns :> columns);
+      insert_const_no dbd uri;
+      insert_name ~dbd ~uri ~name
+    end
 
 let index_inductive_def ~dbd =
   let query = prepare_insert () in
-  fun ~owner ~uri ~types ->
-    let metadata = MetadataExtractor.compute_ind ~uri ~types in
-    let uri_of (a,b,c) = a in
-    let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in
-    let uri = UriManager.string_of_uri uri in
-    let columns = MetadataPp.columns_of_ind_metadata metadata in
-    execute_insert dbd query uri owner (columns :> columns);
-    List.iter (insert_const_no dbd) uris;
-    List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
+  fun ~uri ~types ->
+    if not (already_indexed uri) then begin
+      let metadata = MetadataExtractor.compute_ind ~uri ~types in
+      let uri_of (a,b,c) = a in
+      let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in
+      let uri = UriManager.string_of_uri uri in
+      let columns = MetadataPp.columns_of_ind_metadata metadata in
+      execute_insert dbd query uri (columns :> columns);
+      List.iter (insert_const_no dbd) uris;
+      List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
+    end
+
+let tables_to_clean =
+  [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl]
 
 let clean ~(dbd:Mysql.dbd) =
   let owned_uris =  (* list of uris in list-of-columns format *)
-    let query =
-      (* sprintf 
-       *  "SELECT source FROM %s WHERE owner = \"%s\"" (owners_tbl ())
-       * owner*)
-      sprintf "SELECT source FROM %s" (obj_tbl ())
-    in
+    let query = sprintf "SELECT source FROM %s" (obj_tbl ()) in
     let result = Mysql.exec dbd query in
     let uris = Mysql.map result (fun cols ->
       match cols.(0) with
       | Some src -> src
       | 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)
+    uris
   in
   let del_from tbl =
     let query s = 
@@ -146,8 +142,16 @@ let clean ~(dbd:Mysql.dbd) =
       (fun source_col -> ignore (Mysql.exec dbd (query source_col)))
       owned_uris
   in
-  List.iter del_from
-    [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl(*;
-    owners_tbl*)];
-  List.iter Http_getter.unregister owned_uris  
+  List.iter del_from tables_to_clean;
+  owned_uris
+
+let unindex ~dbd ~uri =
+  let uri = UriManager.string_of_uri uri in
+  let del_from tbl =
+    let query tbl =
+      sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) uri
+    in
+    ignore (Mysql.exec dbd (query tbl))
+  in
+  List.iter del_from tables_to_clean