X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataDb.ml;h=51b432a4f5b843545a1e79eb6adf370d54cd956b;hb=f4c451d39cb4b98e76a291f021c408b3340d2b91;hp=e20e000023e87b8f96a58a9ac629d63fc7e6e2b0;hpb=6fa3218efdfca5dd28fee2ef7a8c5e8de67ce829;p=helm.git

diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml
index e20e00002..51b432a4f 100644
--- a/helm/ocaml/metadata/metadataDb.ml
+++ b/helm/ocaml/metadata/metadataDb.ml
@@ -74,27 +74,27 @@ let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) =
   
     
 let count_distinct position l =
-  MetadataConstraints.StringSet.cardinal
+  MetadataConstraints.UriManagerSet.cardinal
   (List.fold_left (fun acc d -> 
     match position with
     | `Conclusion -> 
          (match d with
          | `Obj (name,`InConclusion) 
          | `Obj (name,`MainConclusion _ ) -> 
-             MetadataConstraints.StringSet.add name acc
+             MetadataConstraints.UriManagerSet.add name acc
          | _ -> acc)
     | `Hypothesis ->
         (match d with
         | `Obj (name,`InHypothesis) 
         | `Obj (name,`MainHypothesis _) -> 
-            MetadataConstraints.StringSet.add name acc
+            MetadataConstraints.UriManagerSet.add name acc
         | _ -> acc)
     | `Statement ->
         (match d with
         | `Obj (name,`InBody) -> acc
-        | `Obj (name,_) -> MetadataConstraints.StringSet.add name acc
+        | `Obj (name,_) -> MetadataConstraints.UriManagerSet.add name acc
         | _ -> acc)
-    ) MetadataConstraints.StringSet.empty l)
+    ) MetadataConstraints.UriManagerSet.empty l)
 (*    
 let insert_const_no dbd uri =
   let term = CicUtil.term_of_uri uri in 
@@ -119,13 +119,13 @@ let insert_const_no dbd (uri,metadata) =
   let no_full = count_distinct `Statement metadata in
   let insert = 
     sprintf "INSERT INTO %s VALUES (\"%s\", %d, %d, %d)" 
-      (count_tbl ()) uri no_concl no_hyp no_full
+      (count_tbl ()) (UriManager.string_of_uri uri) no_concl no_hyp no_full
   in
   ignore (Mysql.exec dbd insert)
   
 let insert_name ~dbd ~uri ~name =
   let query =
-    sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) uri name
+    sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) (UriManager.string_of_uri uri) name
   in
   ignore (Mysql.exec dbd query)
 
@@ -175,12 +175,11 @@ let index_obj ~dbd ~uri =
   
 
 let tables_to_clean =
-  [sort_tbl; rel_tbl; obj_tbl; (*conclno_tbl; fullno_tbl; hypno_tbl;*) name_tbl;
-  count_tbl]
+  [sort_tbl; rel_tbl; obj_tbl; name_tbl; count_tbl]
 
 let clean ~(dbd:Mysql.dbd) =
   let owned_uris =  (* list of uris in list-of-columns format *)
-    let query = sprintf "SELECT source FROM %s" (obj_tbl ()) in
+    let query = sprintf "SELECT source FROM %s" (name_tbl ()) in
     let result = Mysql.exec dbd query in
     let uris = Mysql.map result (fun cols ->
       match cols.(0) with