]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataDb.ml
- clean no longer unregister URIs from the getter, but returns them
[helm.git] / helm / ocaml / metadata / metadataDb.ml
index c56a1a027d6fd900b7aa50c66fec3771cce5d14a..170d02d77229c2c4f4218ac59df500dbf1084973 100644 (file)
@@ -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,46 @@ 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 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 = 
@@ -147,7 +140,6 @@ let clean ~(dbd:Mysql.dbd) =
       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  
+    [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl];
+  owned_uris