Adding a possible DEPRECATED flag to VERNAC EXTEND statements.

4 files changed, 46 insertions, 16 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 650897ef7..f969f0132 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -502,7 +502,7 @@ open Egramml
 
 let _ =
   try
-    Vernacinterp.vinterp_add ("PrintConstr", 0)
+    Vernacinterp.vinterp_add false ("PrintConstr", 0)
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
            let c = out_gen (rawwit wit_constr) c in
@@ -519,7 +519,7 @@ let _ =
 
 let _ =
   try
-    Vernacinterp.vinterp_add ("PrintPureConstr", 0)
+    Vernacinterp.vinterp_add false ("PrintPureConstr", 0)
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
            let c = out_gen (rawwit wit_constr) c in
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index c748d9793..9db89308f 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -26,6 +26,8 @@ type rule = {
   (** An optional classifier for the STM *)
   r_branch : MLast.expr;
   (** The action performed by this rule. *)
+  r_depr : unit option;
+  (** Whether this entry is deprecated *)
 }
 
 let rec make_let e = function
@@ -87,8 +89,15 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
       <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
 
 let make_fun_clauses loc s l =
-  let cl = List.map (fun c -> Compat.make_fun loc [make_clause c]) l in
-  mlexpr_of_list (fun x -> x) cl
+  let map c =
+    let depr = match c.r_depr with
+    | None -> false
+    | Some () -> true
+    in
+    let cl = Compat.make_fun loc [make_clause c] in
+    <:expr< ($mlexpr_of_bool depr$, $cl$)>>
+  in
+  mlexpr_of_list map l
 
 let make_fun_classifiers loc s c l =
   let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
@@ -107,7 +116,7 @@ let declare_command loc s c nt cl =
   declare_str_items loc
     [ <:str_item< do {
 	try do {
-          CList.iteri (fun i f -> Vernacinterp.vinterp_add ($se$, i) f) $funcl$;
+          CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
           CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ }
 	with [ e when Errors.noncritical e ->
 	  Pp.msg_warning
@@ -146,18 +155,23 @@ EXTEND
           <:expr< fun _ -> Vernac_classifier.classify_as_query >>
     ] ]
   ;
+  deprecation:
+    [ [ "DEPRECATED" -> () ] ]
+  ;
   (* spiwack: comment-by-guessing: it seems that the isolated string (which
       otherwise could have been another argument) is not passed to the
       VernacExtend interpreter function to discriminate between the clauses. *)
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
-        c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
       if String.is_empty s then
         Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
-      { r_head = Some s; r_patt = l; r_class = c; r_branch = <:expr< fun () -> $e$ >>; }
+      let b = <:expr< fun () -> $e$ >> in
+      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
       | "[" ; "-" ; l = LIST1 args ; "]" ;
-        c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      { r_head = None; r_patt = l; r_class = c; r_branch = <:expr< fun () -> $e$ >>; }
+        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+      let b = <:expr< fun () -> $e$ >> in
+      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
     ] ]
   ;
   classifier:
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 17f971fda..d3e48f756 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -10,14 +10,17 @@ open Util
 open Pp
 open Errors
 
+type deprecation = bool
+type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
+
 (* Table of vernac entries *)
 let vernac_tab =
   (Hashtbl.create 51 :
-    (Vernacexpr.extend_name, (Genarg.raw_generic_argument list -> unit -> unit)) Hashtbl.t)
+    (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t)
 
-let vinterp_add s f =
+let vinterp_add depr s f =
   try
-    Hashtbl.add vernac_tab s f
+    Hashtbl.add vernac_tab s (depr, f)
   with Failure _ ->
     errorlabstrm "vinterp_add"
       (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
@@ -28,7 +31,7 @@ let overwriting_vinterp_add s f =
       let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s
     with Not_found -> ()
   end;
-  Hashtbl.add vernac_tab s f
+  Hashtbl.add vernac_tab s (false, f)
 
 let vinterp_map s =
   try
@@ -44,7 +47,16 @@ let vinterp_init () = Hashtbl.clear vernac_tab
 let call ?locality (opn,converted_args) =
   let loc = ref "Looking up command" in
   try
-    let callback = vinterp_map opn in
+    let depr, callback = vinterp_map opn in
+    let () = if depr then
+      let rules = Egramml.get_extend_vernac_rule opn in
+      let pr_gram = function
+      | Egramml.GramTerminal s -> str s
+      | Egramml.GramNonTerminal _ -> str "_"
+      in
+      let pr = pr_sequence pr_gram rules in
+      msg_warning (str "Deprecated vernacular command: " ++ pr)
+    in
     loc:= "Checking arguments";
     let hunk = callback converted_args in
     loc:= "Executing command";
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 38fce5d12..028206546 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -8,9 +8,13 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-val vinterp_add : Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
+type deprecation = bool
+type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
+
+val vinterp_add : deprecation -> Vernacexpr.extend_name ->
+  vernac_command -> unit
 val overwriting_vinterp_add :
-  Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
+  Vernacexpr.extend_name -> vernac_command -> unit
 
 val vinterp_init : unit -> unit
 val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit