From d9d4c27ae122d5c413b0e9479de98042e060cea5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Feb 2005 13:02:57 +0000 Subject: [PATCH] locate now searched bot the standard library and the owner(user) library --- helm/ocaml/metadata/metadataTypes.ml | 6 ++++++ helm/ocaml/metadata/metadataTypes.mli | 7 +++++++ helm/ocaml/tactics/metadataQuery.ml | 4 +++- 3 files changed, 16 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index 554282589..9e0d7c0b8 100644 --- 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 86f0df6ec..c471d167a 100644 --- 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 4df0de08b..0a1f1ee44 100644 --- 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 -- 2.39.2