X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fwhelp%2Fwhelp.ml;h=ef544f8502630cfe965f1a2dc4fbabcccd0c3368;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=5e63bcfc4e9078549f202193e66ca2ed91ce3081;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/whelp/whelp.ml b/components/whelp/whelp.ml
index 5e63bcfc4..ef544f850 100644
--- a/components/whelp/whelp.ml
+++ b/components/whelp/whelp.ml
@@ -42,20 +42,33 @@ let sqlpat_of_shellglob =
           (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
             shellglob)))
 
-let locate ~(dbd:HMysql.dbd) ?(vars = false) pat =
+let locate ~(dbd:HSql.dbd) ?(vars = false) pat =
+  let escape dbtype dbd s = HSql.escape dbtype dbd s in
   let sql_pat = sqlpat_of_shellglob pat in
-  let query =
-        sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
-                 "SELECT source FROM %s WHERE value LIKE \"%s\"")
-          (MetadataTypes.name_tbl ()) sql_pat
-           MetadataTypes.library_name_tbl sql_pat
+  let query dbtype tbl =
+        sprintf 
+          ("SELECT source FROM %s WHERE value LIKE \"%s\" "
+           ^^ HSql.escape_string_for_like dbtype dbd)
+          tbl (escape dbtype dbd sql_pat)
   in
-  let result = HMysql.exec dbd query in
-  List.filter nonvar
-    (HMysql.map result
-      (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
+  let tbls = 
+    [HSql.User, MetadataTypes.name_tbl ();
+     HSql.Library, MetadataTypes.library_name_tbl;
+     HSql.Legacy, MetadataTypes.library_name_tbl]
+  in
+  let map cols =
+    match cols.(0) with 
+    | Some s -> UriManager.uri_of_string s | _ -> assert false
+  in
+  let result = 
+    List.fold_left
+      (fun acc (dbtype,tbl) -> 
+         acc @ HSql.map ~f:map (HSql.exec dbtype dbd (query dbtype tbl)))
+      [] tbls
+  in
+  List.filter nonvar result
 
-let match_term ~(dbd:HMysql.dbd) ty =
+let match_term ~(dbd:HSql.dbd) ty =
 (*   debug_print (lazy (CicPp.ppterm ty)); *)
   let metadata = MetadataExtractor.compute ~body:None ~ty in
   let constants_no =
@@ -176,7 +189,7 @@ let instance ~dbd t =
         let constraints_for_dummy_type =
            List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
         (* start with the dummy constant in main conlusion *)
-        let from = ["refObj as table0"] in
+        let from = ["refObj as table0"] in (* XXX table hardcoded *)
         let where = 
           [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
                  sprintf "table0.h_depth >= %d" depth] in
@@ -197,11 +210,15 @@ let instance ~dbd t =
           sprintf "table0.h_depth - table%d.h_depth = %d" 
             n (depth - depth')::where
         in
+        (* XXX performed only in library and legacy not user *)
         let (m,from,where) =
           List.fold_left 
             (MetadataConstraints.add_constraint ~start:n)
-            (n,from,where) constraints_for_dummy_type in
-        MetadataConstraints.exec ~dbd (m,from,where)
+            (n,from,where) constraints_for_dummy_type 
+        in
+        MetadataConstraints.exec HSql.Library ~dbd (m,from,where)
+        @
+        MetadataConstraints.exec HSql.Legacy ~dbd (m,from,where)
 
 let elim ~dbd uri =
   let constraints =