changed "locate" so that it supports shell-like pattern matching with

'*' and '?' wildcards

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 180091c0a871053bcd49c1b997f6ab2bb36421b0..f65318896ae7bd9c57718021fa4df7edc978acb4 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -28,15 +28,29 @@ open Printf
 module Constr = MetadataConstraints
 module PET = ProofEngineTypes 
 
+  (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
+  * the "like" operator (which uses '%' and '_'). Does not support escaping. *)
+let sqlpat_of_shellglob =
+  let star_RE, qmark_RE, percent_RE, uscore_RE =
+    Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_"
+  in
+  fun shellglob ->
+    Pcre.replace ~rex:star_RE ~templ:"%"
+      (Pcre.replace ~rex:qmark_RE ~templ:"_"
+        (Pcre.replace ~rex:percent_RE ~templ:"\\%"
+          (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
+            shellglob)))
+
 let nonvar s =
   let len = String.length s in
   let suffix = String.sub s (len-4) 4 in
   not (suffix  = ".var")
 
-let locate ~(dbd:Mysql.dbd) ?(vars = false) name =
+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 = \"%s\""
-      MetadataTypes.name_tbl name
+    sprintf "SELECT source FROM %s WHERE value LIKE \"%s\""
+      MetadataTypes.name_tbl sql_pat
   in
   let result = Mysql.exec dbd query in
   List.filter nonvar

diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli
index b3b506de96a4e7f15ba87629300b974a0837aa3c..0d32e4835c39ec8442b75bf88e826aa08e7778bd 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.mli
+++ b/helm/ocaml/tactics/metadataQuery.mli
@@ -24,7 +24,9 @@
  *)
 
   (** @param vars if set variables (".var" URIs) are considered. Defaults to
-  * false *)
+  * false
+  * @param pat shell like pattern matching over object names, a string where "*"
+  * is interpreted as 0 or more characters and "?" as exactly one character *)
 val locate:
   dbd:Mysql.dbd ->
   ?vars:bool -> string -> string list