diff options
-rw-r--r-- | ide/ide_slave.ml | 28 | ||||
-rw-r--r-- | toplevel/search.ml | 22 | ||||
-rw-r--r-- | toplevel/search.mli | 4 |
3 files changed, 25 insertions, 29 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 0da08ecd6..3ea3cc6e6 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 = diff --git a/toplevel/search.ml b/toplevel/search.ml index 74a65be67..e670b59b7 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -263,28 +263,6 @@ type search_constraint = | 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; diff --git a/toplevel/search.mli b/toplevel/search.mli index a1814b225..9f209a17e 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -57,10 +57,6 @@ type search_constraint = (** 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; |