]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/metadataQuery.ml
added owner support to the disambiguator (now locate finds only objects
[helm.git] / helm / ocaml / tactics / metadataQuery.ml
index f65318896ae7bd9c57718021fa4df7edc978acb4..4e6b31b537ce880232b591cccc3f9197bd8726dc 100644 (file)
@@ -46,11 +46,23 @@ let nonvar s =
   let suffix = String.sub s (len-4) 4 in
   not (suffix  = ".var")
 
-let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
+let locate ~(dbd:Mysql.dbd) ?(vars = false) ?owner pat =
   let sql_pat = sqlpat_of_shellglob pat in
   let query =
-    sprintf "SELECT source FROM %s WHERE value LIKE \"%s\""
-      MetadataTypes.name_tbl sql_pat
+    match owner with
+    | None -> 
+        sprintf "SELECT source FROM %s WHERE value LIKE \"%s\""
+          MetadataTypes.name_tbl sql_pat
+    | Some owner -> 
+        sprintf "SELECT %s.source FROM %s,%s WHERE 
+                  (%s.source LIKE CONCAT(%s.source,\"#%%\") OR 
+                   %s.source = %s.source) AND
+                  value LIKE \"%s\" AND owner = \"%s\""
+          MetadataTypes.name_tbl
+          MetadataTypes.name_tbl MetadataTypes.owners_tbl
+          MetadataTypes.name_tbl MetadataTypes.owners_tbl
+          MetadataTypes.name_tbl MetadataTypes.owners_tbl
+          sql_pat owner
   in
   let result = Mysql.exec dbd query in
   List.filter nonvar