avoid communicating to the serarch interface using raw strings.

- This patch changes the search interface to take [Str.regexp]s,
  [constr_pattern]s, and [DirPath.t] instead of [string]s and
  [string list]s.
- Convenience functions are provided to do the translation.

3 files changed, 46 insertions, 39 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 9a3e85e47d..0da08ecd66 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -282,10 +282,10 @@ let export_coq_object t = {
 }
 
 let import_search_constraint = function
-  | Interface.Name_Pattern s    -> Search.Name_Pattern s
-  | Interface.Type_Pattern s    -> Search.Type_Pattern s
-  | Interface.SubType_Pattern s -> Search.SubType_Pattern s
-  | Interface.In_Module ms      -> Search.In_Module ms
+  | Interface.Name_Pattern s    -> Search.Name_Pattern (Str.regexp s)
+  | Interface.Type_Pattern s    -> Search.Type_Pattern (Search.pattern_of_string s)
+  | Interface.SubType_Pattern s -> Search.SubType_Pattern (Search.pattern_of_string s)
+  | Interface.In_Module ms      -> Search.In_Module (Search.dirpath_of_string_list ms)
   | Interface.Include_Blacklist -> Search.Include_Blacklist
 
 let search flags =
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 646e2e08ac..74a65be67d 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -257,52 +257,55 @@ let search_about gopt items mods =
   format_display !ans
 
 type search_constraint =
-  | Name_Pattern of string
-  | Type_Pattern of string
-  | SubType_Pattern of string
-  | In_Module of string list
+  | Name_Pattern of Str.regexp
+  | Type_Pattern of Pattern.constr_pattern
+  | SubType_Pattern of Pattern.constr_pattern
+  | In_Module of Names.DirPath.t
   | Include_Blacklist
 
+let pattern_of_string ?env s =
+  let env =
+    match env with
+    | None -> Global.env ()
+    | Some e -> e
+  in
+  let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
+  let (_, pat) = Constrintern.intern_constr_pattern env constr in
+  pat
+
+let dirpath_of_string_list s =
+  let path = String.concat "." s in
+  let m = Pcoq.parse_string Pcoq.Constr.global path in
+  let (_, qid) = Libnames.qualid_of_reference m in
+  let id =
+    try Nametab.full_name_module qid
+    with Not_found ->
+      Errors.errorlabstrm "Search.interface_search"
+        (str "Module " ++ str path ++ str " not found.")
+  in
+  id
+
 type 'a coq_object = {
   coq_object_prefix : string list;
   coq_object_qualid : string list;
   coq_object_object : 'a;
 }
 
-let interface_search flags =
-  let env = Global.env () in
+let interface_search =
   let rec extract_flags name tpe subtpe mods blacklist = function
   | [] -> (name, tpe, subtpe, mods, blacklist)
-  | (Name_Pattern s, b) :: l ->
-    let regexp =
-      try Str.regexp s
-      with e when Errors.noncritical e ->
-        Errors.errorlabstrm "Search.interface_search"
-          (str "Invalid regexp: " ++ str s)
-    in
+  | (Name_Pattern regexp, b) :: l ->
     extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
-  | (Type_Pattern s, b) :: l ->
-    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-    let (_, pat) = Constrintern.intern_constr_pattern env constr in
+  | (Type_Pattern pat, b) :: l ->
     extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
-  | (SubType_Pattern s, b) :: l ->
-    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-    let (_, pat) = Constrintern.intern_constr_pattern env constr in
+  | (SubType_Pattern pat, b) :: l ->
     extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
-  | (In_Module m, b) :: l ->
-    let path = String.concat "." m in
-    let m = Pcoq.parse_string Pcoq.Constr.global path in
-    let (_, qid) = Libnames.qualid_of_reference m in
-    let id =
-      try Nametab.full_name_module qid
-      with Not_found ->
-        Errors.errorlabstrm "Search.interface_search"
-          (str "Module " ++ str path ++ str " not found.")
-    in
+  | (In_Module id, b) :: l ->
     extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
   | (Include_Blacklist, b) :: l ->
     extract_flags name tpe subtpe mods b l
   in
+  fun ?glnum flags ->
   let (name, tpe, subtpe, mods, blacklist) =
     extract_flags [] [] [] [] false flags
   in
@@ -359,5 +362,5 @@ let interface_search flags =
   let iter ref env typ =
     if filter_function ref env typ then print_function ref env typ
   in
-  let () = generic_search None iter in (* TODO: chose a goal number? *)
+  let () = generic_search glnum iter in
   !ans
diff --git a/toplevel/search.mli b/toplevel/search.mli
index 78b0c45c01..a1814b2257 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -47,23 +47,27 @@ val search_about   : int option -> (bool * glob_search_about_item) list
 
 type search_constraint =
   (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
-  | Name_Pattern of string
+  | Name_Pattern of Str.regexp
   (** Whether the object type satisfies a pattern *)
-  | Type_Pattern of string
+  | Type_Pattern of Pattern.constr_pattern
   (** Whether some subtype of object type satisfies a pattern *)
-  | SubType_Pattern of string
+  | SubType_Pattern of Pattern.constr_pattern
   (** Whether the object pertains to a module *)
-  | In_Module of string list
+  | In_Module of Names.DirPath.t
   (** Bypass the Search blacklist *)
   | Include_Blacklist
 
+val pattern_of_string : ?env:Environ.env -> string -> Pattern.constr_pattern
+
+val dirpath_of_string_list : string list -> Names.DirPath.t
+
 type 'a coq_object = {
   coq_object_prefix : string list;
   coq_object_qualid : string list;
   coq_object_object : 'a;
 }
 
-val interface_search : (search_constraint * bool) list ->
+val interface_search : ?glnum:int -> (search_constraint * bool) list ->
   string coq_object list
 
 (** {6 Generic search function} *)