locate now searched bot the standard library and the owner(user) library

diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml
index 5542825893d65369c9099bb36579d51abdb98d31..9e0d7c0b87a48f517cf4b136512469eeeabb30e6 100644 (file)
--- a/helm/ocaml/metadata/metadataTypes.ml
+++ b/helm/ocaml/metadata/metadataTypes.ml
@@ -97,4 +97,10 @@ let ownerize_tables owner =
   name_tbl_real := ( name_tbl_original ^ "_" ^ owner) 
 ;;
 
+let library_sort_tbl =   sort_tbl_original
+let library_rel_tbl = rel_tbl_original
+let library_obj_tbl = obj_tbl_original
+let library_conclno_tbl = conclno_tbl_original
+let library_conclno_hyp_tbl = conclno_hyp_tbl_original
+let library_name_tbl = name_tbl_original
 

diff --git a/helm/ocaml/metadata/metadataTypes.mli b/helm/ocaml/metadata/metadataTypes.mli
index 86f0df6ece47411f9e57d0d6502549384030641d..c471d167a48014c6cad61a58ba63e28091d80dd0 100644 (file)
--- a/helm/ocaml/metadata/metadataTypes.mli
+++ b/helm/ocaml/metadata/metadataTypes.mli
@@ -68,3 +68,10 @@ val conclno_tbl: unit -> string
 val conclno_hyp_tbl: unit -> string
 val name_tbl: unit -> string
 
+val library_sort_tbl:  string  
+val library_rel_tbl:  string
+val library_obj_tbl:  string
+val library_conclno_tbl:  string
+val library_conclno_hyp_tbl:  string
+val library_name_tbl:  string
+

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 4df0de08b93c5add8d741cfd17136898c56be249..0a1f1ee441e939f22e9364b1806c626db1ada685 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -49,8 +49,10 @@ let nonvar s =
 let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
   let sql_pat = sqlpat_of_shellglob pat in
   let query =
-        sprintf "SELECT source FROM %s WHERE value LIKE \"%s\""
+        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
   in
   let result = Mysql.exec dbd query in
   List.filter nonvar