Backport PR rocq-prover#20839: [classifier] visibility on attributes

Author: gares

coqpp/coqpp_main.ml

@@ -369,9 +369,9 @@ let print_rule_classifier fmt r = match r.vernac_class with
 | Some f ->
   let no_binder = function ExtTerminal _ -> true | ExtNonTerminal _ -> false in
   if List.for_all no_binder r.vernac_toks then
-    fprintf fmt "Some @[%a@]" print_code f
+    fprintf fmt "Some @[(fun ~atts -> %a)@]" print_code f
   else
-    fprintf fmt "Some @[(fun %a-> %a)@]" print_binders r.vernac_toks print_code f
+    fprintf fmt "Some @[(fun %a ~atts -> %a)@]" print_binders r.vernac_toks print_code f
 
 (* let print_atts fmt = function *)
 (*   | None -> fprintf fmt "@[let () = Attributes.unsupported_attributes atts in@] " *)
@@ -482,11 +482,11 @@ let print_classifier fmt = function
    when the block level classifier is specified *)
 | ClassifDefault -> fprintf fmt ""
 | ClassifName "QUERY" ->
-  fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_query)"
+  fprintf fmt "~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_query)"
 | ClassifName "SIDEFF" ->
-  fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_sideeff)"
+  fprintf fmt "~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_sideeff)"
 | ClassifName s -> fatal (Printf.sprintf "Unknown classifier %s" s)
-| ClassifCode c -> fprintf fmt "~classifier:(%s)" c.code
+| ClassifCode c -> fprintf fmt "~classifier:(fun ~atts -> %s)" c.code
 
 let print_entry fmt = function
 | None -> fprintf fmt "None"

dev/ci/user-overlays/20839-gares-vernac-class-atts.sh

@@ -0,0 +1,3 @@
+overlay elpi https://github.com/gares/coq-elpi vernac-class-atts 20839
+
+overlay metarocq https://github.com/gares/metarocq vernac-class-atts 20839

dev/top_printers.ml

@@ -664,7 +664,7 @@ let () =
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
   let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context econstr_display c) in
-  let cmd_class _ = VtQuery in
+  let cmd_class _ ~atts:_ = VtQuery in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   static_vernac_extend ~plugin:None ~command:"PrintConstr" [cmd]
 
@@ -674,7 +674,7 @@ let () =
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
   let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context print_pure_econstr c) in
-  let cmd_class _ = VtQuery in
+  let cmd_class _ ~atts:_ = VtQuery in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   static_vernac_extend ~plugin:None ~command:"PrintPureConstr" [cmd]
 

vernac/vernac_classifier.ml

@@ -83,7 +83,7 @@ let classify_vernac e =
     (* Plugins should classify their commands *)
     | VernacLoad _ -> VtSideff ([], VtNow)
     | VernacExtend (s,l) ->
-        try Vernacextend.get_vernac_classifier s l
+        try Vernacextend.get_vernac_classifier s ~atts l
         with Not_found -> anomaly(str"No classifier for"++spc()++str s.ext_entry ++str".")
   in
   let static_pure_classifier ~atts e = match e with

vernac/vernacextend.ml

@@ -92,7 +92,10 @@ let type_vernac opn converted_args ?loc ~atts =
 
 (** VERNAC EXTEND registering *)
 
-type classifier = Genarg.raw_generic_argument list -> vernac_classification
+type classifier =
+  Genarg.raw_generic_argument list ->
+  atts:Attributes.vernac_flags ->
+  vernac_classification
 
 (** Classifiers  *)
 module StringPair =
@@ -119,7 +122,7 @@ let classify_as_sideeff = VtSideff ([], VtLater)
 let classify_as_proofstep = VtProofStep { proof_block_detection = None}
 
 type (_, _) ty_sig =
-| TyNil : (vernac_command, vernac_classification) ty_sig
+| TyNil : (vernac_command, atts:Attributes.vernac_flags -> vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
@@ -199,7 +202,7 @@ let static_vernac_extend ~plugin ~command ?classifier ?entry ext =
   | Some cl -> untype_classifier ty cl
   | None ->
     match classifier with
-    | Some cl -> fun _ -> cl command
+    | Some cl -> fun _ ~atts -> cl ~atts command
     | None ->
       let e = match entry with
       | None -> "COMMAND"

vernac/vernacextend.mli

@@ -75,10 +75,13 @@ val type_vernac : Vernacexpr.extend_name -> plugin_args -> vernac_command
 
 (** {5 VERNAC EXTEND} *)
 
-type classifier = Genarg.raw_generic_argument list -> vernac_classification
+type classifier =
+  Genarg.raw_generic_argument list ->
+  atts:Attributes.vernac_flags ->
+  vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (vernac_command, vernac_classification) ty_sig
+| TyNil : (vernac_command, atts:Attributes.vernac_flags -> vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
@@ -100,7 +103,7 @@ type ty_ml = TyML : bool (* deprecated *) * ('r, 's) ty_sig * 'r * 's option ->
 val static_vernac_extend :
   plugin:string option ->
   command:string ->
-  ?classifier:(string -> vernac_classification) ->
+  ?classifier:(atts:Attributes.vernac_flags -> string -> vernac_classification) ->
   ?entry:Vernacexpr.vernac_expr Procq.Entry.t ->
   ty_ml list -> unit