diff options
Diffstat (limited to 'toplevel/vernacinterp.ml')
| -rw-r--r-- | toplevel/vernacinterp.ml | 34 |
1 files changed, 14 insertions, 20 deletions
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 0a94c050..17f971fd 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -1,35 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Util -open Names -open Libnames -open Himsg -open Proof_type -open Tacinterp -open Vernacexpr - -let disable_drop e = - if e <> Drop then e - else UserError("Vernac.disable_drop",(str"Drop is forbidden.")) +open Pp +open Errors (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 51 : - (string, Tacexpr.raw_generic_argument list -> unit -> unit) Hashtbl.t) + (Vernacexpr.extend_name, (Genarg.raw_generic_argument list -> unit -> unit)) Hashtbl.t) let vinterp_add s f = try Hashtbl.add vernac_tab s f with Failure _ -> errorlabstrm "vinterp_add" - (str"Cannot add the vernac command " ++ str s ++ str" twice.") + (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") let overwriting_vinterp_add s f = begin @@ -42,25 +33,28 @@ let overwriting_vinterp_add s f = let vinterp_map s = try Hashtbl.find vernac_tab s - with Not_found -> + with Failure _ | Not_found -> errorlabstrm "Vernac Interpreter" - (str"Cannot find vernac command " ++ str s ++ str".") + (str"Cannot find vernac command " ++ str (fst s) ++ str".") let vinterp_init () = Hashtbl.clear vernac_tab (* Interpretation of a vernac command *) -let call (opn,converted_args) = +let call ?locality (opn,converted_args) = let loc = ref "Looking up command" in try let callback = vinterp_map opn in loc:= "Checking arguments"; let hunk = callback converted_args in loc:= "Executing command"; - hunk() + Locality.LocalityFixme.set locality; + hunk(); + Locality.LocalityFixme.assert_consumed() with | Drop -> raise Drop | reraise -> + let reraise = Errors.push reraise in if !Flags.debug then - msgnl (str"Vernac Interpreter " ++ str !loc); - raise reraise + msg_debug (str"Vernac Interpreter " ++ str !loc); + iraise reraise |