X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fwhelp%2Fwhelp.ml;h=ef544f8502630cfe965f1a2dc4fbabcccd0c3368;hb=5717dca7637e00f6f82e462619ee0e07d99cf289;hp=eb1f2b6301c239611b7fa88eb7021ffe78333612;hpb=190662b877ba89ccb152f0bf5c67df62be737335;p=helm.git

diff --git a/components/whelp/whelp.ml b/components/whelp/whelp.ml
index eb1f2b630..ef544f850 100644
--- a/components/whelp/whelp.ml
+++ b/components/whelp/whelp.ml
@@ -43,20 +43,30 @@ let sqlpat_of_shellglob =
             shellglob)))
 
 let locate ~(dbd:HSql.dbd) ?(vars = false) pat =
-  let escape s = HSql.escape s in
+  let escape dbtype dbd s = HSql.escape dbtype dbd s in
   let sql_pat = sqlpat_of_shellglob pat in
-  let query =
+  let query dbtype tbl =
         sprintf 
-          ("SELECT source FROM %s WHERE value LIKE \"%s\" ESCAPE \"\\\" "
-           ^^ "UNION " ^^
-           "SELECT source FROM %s WHERE value LIKE \"%s\" ESCAPE \"\\\" ")
-          (MetadataTypes.name_tbl ()) (escape sql_pat)
-           MetadataTypes.library_name_tbl (escape sql_pat)
+          ("SELECT source FROM %s WHERE value LIKE \"%s\" "
+           ^^ HSql.escape_string_for_like dbtype dbd)
+          tbl (escape dbtype dbd sql_pat)
   in
-  let result = HSql.exec dbd query in
-  List.filter nonvar
-    (HSql.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:HSql.dbd) ty =
 (*   debug_print (lazy (CicPp.ppterm ty)); *)
@@ -179,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
@@ -200,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 =