Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules

6 files changed, 18 insertions, 18 deletions

diff --git a/API/API.mli b/API/API.mli
index 589745b61..ccb71179d 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5831,7 +5831,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