diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-11 18:35:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-11 18:35:31 +0000 |
| commit | 76dfe2df5a5fc4623384a04610ba9f73030fee60 (patch) | |
| tree | fd2dca003e37beb1d4cfa6d21f655ccc0edbd8b5 /toplevel | |
| parent | 2e6c3a7b0b12cfd3b560de60f4918063f149fd01 (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 15 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
2 files changed, 15 insertions, 4 deletions
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 |