From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Feb 2005 13:02:57 +0000 (+0000)
Subject: locate now searched bot the standard library and the owner(user) library
X-Git-Tag: V_0_1_0~22
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d9d4c27ae122d5c413b0e9479de98042e060cea5;p=helm.git

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 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