Only parsing in Reserved Notation: turning notice into a warning.

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 *)