From 76dfe2df5a5fc4623384a04610ba9f73030fee60 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 11 Oct 2008 18:35:31 +0000 Subject: Backporting 11445 from 8.2 to trunk (negative conditions in SearchAbout + referring objects by their notation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11446 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/vernacentries.ml | 15 +++++++++++++-- toplevel/vernacexpr.ml | 4 ++-- 2 files changed, 15 insertions(+), 4 deletions(-) (limited to 'toplevel') diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8c0e7e05a..d1c972e2b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1107,9 +1107,20 @@ let interp_search_restriction = function open Search +let is_ident s = try ignore (check_ident s); true with UserError _ -> false + let interp_search_about_item = function | SearchRef r -> GlobSearchRef (global_with_alias r) - | SearchString s -> GlobSearchString s + | SearchString (s,None) when is_ident s -> GlobSearchString s + | SearchString (s,sc) -> + try + let ref = + Notation.interp_notation_as_global_reference dummy_loc + (fun _ -> true) s sc in + GlobSearchRef ref + with UserError _ -> + error ("Unable to interp \""^s^"\" either as a reference or + as an identifier component") let vernac_search s r = let r = interp_search_restriction r in @@ -1124,7 +1135,7 @@ let vernac_search s r = | SearchHead ref -> Search.search_by_head (global_with_alias ref) r | SearchAbout sl -> - Search.search_about (List.map interp_search_about_item sl) r + Search.search_about (List.map (on_snd interp_search_about_item) sl) r let vernac_locate = function | LocateTerm qid -> msgnl (print_located_qualid qid) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 86b052d47..19b913708 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -70,13 +70,13 @@ type printable = type search_about_item = | SearchRef of reference - | SearchString of string + | SearchString of string * scope_name option type searchable = | SearchPattern of pattern_expr | SearchRewrite of pattern_expr | SearchHead of reference - | SearchAbout of search_about_item list + | SearchAbout of (bool * search_about_item) list type locatable = | LocateTerm of reference -- cgit v1.2.3