From 9dc88f3c146aeaf8151fcef6ac45ca50675d052b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 14 Feb 2020 09:12:48 +0100 Subject: Only parsing in Reserved Notation: turning notice into a warning. --- theories/ssr/ssrbool.v | 10 +++++----- theories/ssr/ssreflect.v | 6 +++--- vernac/metasyntax.ml | 26 +++++++++++++++----------- 3 files changed, 23 insertions(+), 19 deletions(-) diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index 475859fcc2..e2ab812cce 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -437,7 +437,7 @@ Reserved Notation "{ 'on' cd , 'bijective' f }" (at level 0, f at level 8, is | or => . It is important that in other notations a leading square bracket #[# is always followed by an operator symbol or a fixed identifier. **) -Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing). +Reserved Notation "[ /\ P1 & P2 ]" (at level 0). Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format "'[hv' [ /\ '[' P1 , '/' P2 ']' '/ ' & P3 ] ']'"). Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format @@ -445,21 +445,21 @@ Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format Reserved Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" (at level 0, format "'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 , '/' P4 ']' '/ ' & P5 ] ']'"). -Reserved Notation "[ \/ P1 | P2 ]" (at level 0, only parsing). +Reserved Notation "[ \/ P1 | P2 ]" (at level 0). Reserved Notation "[ \/ P1 , P2 | P3 ]" (at level 0, format "'[hv' [ \/ '[' P1 , '/' P2 ']' '/ ' | P3 ] ']'"). Reserved Notation "[ \/ P1 , P2 , P3 | P4 ]" (at level 0, format "'[hv' [ \/ '[' P1 , '/' P2 , '/' P3 ']' '/ ' | P4 ] ']'"). -Reserved Notation "[ && b1 & c ]" (at level 0, only parsing). +Reserved Notation "[ && b1 & c ]" (at level 0). Reserved Notation "[ && b1 , b2 , .. , bn & c ]" (at level 0, format "'[hv' [ && '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' & c ] ']'"). -Reserved Notation "[ || b1 | c ]" (at level 0, only parsing). +Reserved Notation "[ || b1 | c ]" (at level 0). Reserved Notation "[ || b1 , b2 , .. , bn | c ]" (at level 0, format "'[hv' [ || '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' | c ] ']'"). -Reserved Notation "[ ==> b1 => c ]" (at level 0, only parsing). +Reserved Notation "[ ==> b1 => c ]" (at level 0). Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format "'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'"). diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v index bc4a57dedd..701ebcad56 100644 --- a/theories/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v @@ -97,11 +97,11 @@ Local Notation CoqCast x T := (x : T) (only parsing). (** Reserve notation that introduced in this file. **) Reserved Notation "'if' c 'then' vT 'else' vF" (at level 200, - c, vT, vF at level 200, only parsing). + c, vT, vF at level 200). Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200, - c, R, vT, vF at level 200, only parsing). + c, R, vT, vF at level 200). Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200, - c, R, vT, vF at level 200, x ident, only parsing). + c, R, vT, vF at level 200, x ident). Reserved Notation "x : T" (at level 100, right associativity, format "'[hv' x '/ ' : T ']'"). diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index d39ee60c25..f2e1002f71 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1157,7 +1157,7 @@ let find_precedence custom lev etyps symbols onlyprint = | (ETIdent | ETBigint | ETString | ETGlobal), _ -> begin match lev with | None -> - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) + ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")],0) | Some 0 -> ([],0) | _ -> @@ -1174,7 +1174,7 @@ let find_precedence custom lev etyps symbols onlyprint = else [],Option.get lev) | Some (Terminal _) when last_is_terminal () -> if Option.is_empty lev then - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) + ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")], 0) else [],Option.get lev | Some _ -> if Option.is_empty lev then user_err Pp.(str "Cannot determine the level."); @@ -1227,7 +1227,7 @@ module SynData = struct extra : (string * string) list; (* XXX: Callback to printing, must remove *) - msgs : ((Pp.t -> unit) * Pp.t) list; + msgs : (unit -> unit) list; (* Fields for internalization *) recvars : (Id.t * Id.t) list; @@ -1325,15 +1325,19 @@ let compute_syntax_data ~local deprecation df modifiers = not_data = sy_fulldata; } +let warn_only_parsing_reserved_notation = + CWarnings.create ~name:"irrelevant-reserved-notation-only-parsing" ~category:"parsing" + (fun () -> strbrk "The only parsing modifier has no effect in Reserved Notation.") + let compute_pure_syntax_data ~local df mods = let open SynData in let sd = compute_syntax_data ~local None df mods in - let msgs = - if sd.only_parsing then - (Feedback.msg_warning ?loc:None, - strbrk "The only parsing modifier has no effect in Reserved Notation.")::sd.msgs - else sd.msgs in - { sd with msgs } + if sd.only_parsing + then + let msgs = (fun () -> warn_only_parsing_reserved_notation ?loc:None ())::sd.msgs in + { sd with msgs; only_parsing = false } + else + sd (**********************************************************************) (* Registration of notations interpretation *) @@ -1518,7 +1522,7 @@ let add_notation_in_scope ~local deprecation df env c mods scope = notobj_notation = sd.info; } in (* Ready to change the global state *) - Flags.if_verbose (List.iter (fun (f,x) -> f x)) sd.msgs; + List.iter (fun f -> f ()) sd.msgs; Lib.add_anonymous_leaf (inSyntaxExtension (local, sy_rules)); Lib.add_anonymous_leaf (inNotation notation); sd.info @@ -1565,7 +1569,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in let psd = compute_pure_syntax_data ~local df mods in let sy_rules = make_syntax_rules {psd with deprecation = None} in - Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs; + List.iter (fun f -> f ()) psd.msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) (* Notations with only interpretation *) -- cgit v1.2.3