From 03d5d707a6d6b2cf88b7a3c9d044ec035e2efb5a Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Sun, 24 Apr 2016 13:23:20 -0700
Subject: 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.
---
 ide/ide_slave.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'ide')

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 =
-- 
cgit v1.2.3


From 296e30761a183e64ab9c5e8dc8f2b0e48334735f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Jun 2016 23:14:26 +0200
Subject: Removing the convenience functions from the Search API.

---
 ide/ide_slave.ml | 28 +++++++++++++++++++++++++---
 1 file changed, 25 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 0da08ecd66..3ea3cc6e63 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -281,11 +281,33 @@ let export_coq_object t = {
   Interface.coq_object_object = t.Search.coq_object_object
 }
 
+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
+
 let import_search_constraint = function
   | 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.Type_Pattern s    -> Search.Type_Pattern (pattern_of_string s)
+  | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s)
+  | Interface.In_Module ms      -> Search.In_Module (dirpath_of_string_list ms)
   | Interface.Include_Blacklist -> Search.Include_Blacklist
 
 let search flags =
-- 
cgit v1.2.3