diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-23 11:08:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-23 11:08:27 +0100 |
| commit | 95d1ba0636d95e213f327fc9dba9002b29e95da6 (patch) | |
| tree | fa70e88054365c1bd97976ee64199ef36021f441 /toplevel | |
| parent | f1389e10e6bf15e0fe3fd120f4aa8e59579a16b4 (diff) | |
| parent | f7dfa9d5e1195b8db3711126f953c1605e8cfcf2 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacinterp.ml | 22 | ||||
| -rw-r--r-- | toplevel/vernacinterp.mli | 8 |
2 files changed, 23 insertions, 7 deletions
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 |