From f874a292c94b290a31af8e0f707ffd20ab31001b Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Fri, 4 Aug 2017 18:28:31 +0200 Subject: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules Originally, it was not possible to define a new vernacular command in the following way: VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY [ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ] END because "loc : Loc.t" was not bound. This commit fixes that, i.e. the location of the custom Vernacular command (within *.v file) is made available as "loc" variable bound on the right side of "->" . --- API/API.mli | 2 +- dev/top_printers.ml | 4 ++-- grammar/vernacextend.mlp | 10 +++++----- vernac/vernacentries.ml | 2 +- vernac/vernacinterp.ml | 14 +++++++------- vernac/vernacinterp.mli | 4 ++-- 6 files changed, 18 insertions(+), 18 deletions(-) diff --git a/API/API.mli b/API/API.mli index e20793077..e82297202 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5814,7 +5814,7 @@ module Vernacinterp : sig type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> unit -> unit + type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 70f7c4283..35956477d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -503,7 +503,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun () -> in_current_context constr_display c) + (fun _ -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) @@ -519,7 +519,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun () -> in_current_context print_pure_constr c) + (fun _ -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index a529185dd..874712124 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -59,7 +59,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = | None, Some cg -> (make_patt pt, ploc_vala None, - <:expr< fun () -> $cg$ $str:s$ >>) + <:expr< fun loc -> $cg$ $str:s$ >>) | None, None -> prerr_endline (("Vernac entry \""^s^"\" misses a classifier. "^ "A classifier is a function that returns an expression "^ @@ -82,7 +82,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, ploc_vala None, - <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = let map c = @@ -165,16 +165,16 @@ EXTEND [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> let () = if s = "" then failwith "Command name is empty." in - let b = <:expr< fun () -> $e$ >> in + let b = <:expr< fun loc -> $e$ >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun () -> $e$ >> in + let b = <:expr< fun loc -> $e$ >> in { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } ] ] ; classifier: - [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ] ] + [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ] ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e08cb8387..f83546ea6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2070,7 +2070,7 @@ let interp ?proof ?loc locality poly c = | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] (* Extensions *) - | VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args) + | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args) (* Vernaculars that take a locality flag *) let check_vernac_supports_locality c l = diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 2d9c0fa36..41fee6bd0 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -11,7 +11,7 @@ open Pp open CErrors type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> unit -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit (* Table of vernac entries *) let vernac_tab = @@ -49,8 +49,8 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) -let call ?locality (opn,converted_args) = - let loc = ref "Looking up command" in +let call ?locality ?loc (opn,converted_args) = + let phase = ref "Looking up command" in try let depr, callback = vinterp_map opn in let () = if depr then @@ -62,16 +62,16 @@ let call ?locality (opn,converted_args) = let pr = pr_sequence pr_gram rules in warn_deprecated_command pr; in - loc:= "Checking arguments"; + phase := "Checking arguments"; let hunk = callback converted_args in - loc:= "Executing command"; + phase := "Executing command"; Locality.LocalityFixme.set locality; - hunk(); + hunk loc; 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); + Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); iraise reraise diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index f58d07086..84370fdc2 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -9,7 +9,7 @@ (** Interpretation of extended vernac phrases. *) type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> unit -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit @@ -17,4 +17,4 @@ val overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit val vinterp_init : unit -> unit -val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit +val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit -- cgit v1.2.3