diff options
| author | Maxime Dénès | 2019-07-26 13:51:15 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-30 12:37:13 +0100 |
| commit | a394876327dbe8af8410e8e91c01a363fd2d4cdf (patch) | |
| tree | 58cf4a1a4b8969e05db28fec343cbc2d1a6ffe7b | |
| parent | cd8c4fc982c874802546769b1f7df3c2dcfc0579 (diff) | |
Actually deprecate `SearchAbout`
Fixes #10573
| -rw-r--r-- | vernac/g_vernac.mlg | 2 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 1 |
4 files changed, 12 insertions, 1 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 8d6724c3b1..5f088379ca 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1003,7 +1003,7 @@ GRAMMAR EXTEND Gram | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> { fun g -> VernacSearch (SearchRewrite c,g, l) } | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> - { let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) } + { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) } (* compatibility: SearchAbout *) | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 080629ede2..1aa9a4e0f5 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -161,6 +161,8 @@ open Pputils | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchAbout sl -> + keyword "SearchAbout" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + | Search sl -> keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b let pr_option_ref_value = function diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 535aceed15..bb55cd5114 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1785,6 +1785,10 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } +let warn_deprecated_search_about = + CWarnings.create ~name:"deprecated-search-about" ~category:"deprecated" + (fun () -> strbrk "The SearchAbout command is deprecated. Please use Search instead.") + let vernac_search ~pstate ~atts s gopt r = let gopt = query_command_selector gopt in let r = interp_search_restriction r in @@ -1815,6 +1819,10 @@ let vernac_search ~pstate ~atts s gopt r = | SearchHead c -> (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchAbout sl -> + warn_deprecated_search_about (); + (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + Search.prioritize_search) pr_search + | Search sl -> (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> Search.prioritize_search) pr_search diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ce96d9265c..bec6a0d2bb 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -70,6 +70,7 @@ type searchable = | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr | SearchAbout of (bool * search_about_item) list + | Search of (bool * search_about_item) list type locatable = | LocateAny of qualid or_by_notation |