Merge PR #12341: [search] [ssr] Emit deprecated message when calling search from ssreflect

Reviewed-by: Zimmi48
Ack-by: gares

4 files changed, 39 insertions, 1 deletions

diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 7ef3e44848..24772a8514 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -300,6 +300,35 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
           Ssrview.AdaptorDb.declare k hints }
 END
 
+(** Search compatibility *)
+
+{
+
+  let warn_search_moved_enabled = ref true
+  let warn_search_moved = CWarnings.create ~name:"ssr-search-moved"
+      ~category:"deprecated" ~default:CWarnings.Enabled
+      (fun () ->
+         (Pp.strbrk
+            "SSReflect's Search command has been moved to the \
+             ssrsearch module; please Require that module if you \
+             still want to use SSReflect's Search command"))
+
+open G_vernac
+}
+
+GRAMMAR EXTEND Gram
+  GLOBAL: query_command;
+
+  query_command:
+    [ [ IDENT "Search"; s = search_query; l = search_queries; "." ->
+          { let (sl,m) = l in
+            if !warn_search_moved_enabled then warn_search_moved ();
+            fun g ->
+              Vernacexpr.VernacSearch (Vernacexpr.Search (s::sl),g, m) }
+      ] ]
+;
+END
+
 (** Keyword compatibility fixes. *)
 
 (* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *)
diff --git a/plugins/ssr/ssrvernac.mli b/plugins/ssr/ssrvernac.mli
index 327a2d4660..93339313f0 100644
--- a/plugins/ssr/ssrvernac.mli
+++ b/plugins/ssr/ssrvernac.mli
@@ -9,3 +9,5 @@
 (************************************************************************)
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+
+val warn_search_moved_enabled : bool ref
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 1651e1cc71..6d68cc13ab 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -299,6 +299,10 @@ let ssrdisplaysearch gr env t =
   let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
   Feedback.msg_notice (hov 2 pr_res ++ fnl ())
 
+(* Remove the warning entirely when this plugin is loaded. *)
+let _ =
+  Ssreflect_plugin.Ssrvernac.warn_search_moved_enabled := false
+
 let deprecated_search =
   CWarnings.create
     ~name:"deprecated-ssr-search"
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index fe3bb9b890..45bf61d79e 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -35,6 +35,9 @@ open Attributes
 
 let query_command = Entry.create "vernac:query_command"
 
+let search_query = Entry.create "vernac:search_query"
+let search_queries = Entry.create "vernac:search_queries"
+
 let subprf = Entry.create "vernac:subprf"
 
 let quoted_attributes = Entry.create "vernac:quoted_attributes"
@@ -819,7 +822,7 @@ GRAMMAR EXTEND Gram
 END
 
 GRAMMAR EXTEND Gram
-  GLOBAL: command query_command class_rawexpr gallina_ext;
+  GLOBAL: command query_command class_rawexpr gallina_ext search_query search_queries;
 
   gallina_ext:
     [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->