diff options
Diffstat (limited to 'vernac/vernacinterp.ml')
-rw-r--r-- | vernac/vernacinterp.ml | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml new file mode 100644 index 000000000..f26ef460d --- /dev/null +++ b/vernac/vernacinterp.ml @@ -0,0 +1,77 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open CErrors + +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, deprecation * vernac_command) Hashtbl.t) + +let vinterp_add depr s f = + try + Hashtbl.add vernac_tab s (depr, f) + with Failure _ -> + user_err ~hdr:"vinterp_add" + (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") + +let overwriting_vinterp_add s f = + begin + try + let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s + with Not_found -> () + end; + Hashtbl.add vernac_tab s (false, f) + +let vinterp_map s = + try + Hashtbl.find vernac_tab s + with Failure _ | Not_found -> + user_err ~hdr:"Vernac Interpreter" + (str"Cannot find vernac command " ++ str (fst s) ++ str".") + +let vinterp_init () = Hashtbl.clear vernac_tab + +let warn_deprecated_command = + let open CWarnings in + create ~name:"deprecated-command" ~category:"deprecated" + (fun pr -> str "Deprecated vernacular command: " ++ pr) + +(* Interpretation of a vernac command *) + +let call ?locality (opn,converted_args) = + let loc = ref "Looking up command" in + try + 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 + warn_deprecated_command pr; + in + loc:= "Checking arguments"; + let hunk = callback converted_args in + loc:= "Executing command"; + Locality.LocalityFixme.set locality; + hunk(); + Locality.LocalityFixme.assert_consumed() + with + | Drop -> raise Drop + | reraise -> + let reraise = CErrors.push reraise in + if !Flags.debug then + Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc); + iraise reraise |