From 4b3a261bee1882c338e6e72e992349dfa02f9678 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Tue, 28 Jun 2016 10:55:30 +0200
Subject: A new infrastructure for warnings.

On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.

We also provide a vernacular Set Warnings which takes the same flags as argument.

Note that coqc now prints warnings.

The name and category of a warning are printed with the warning itself.

On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:

1) create it by:

let warn_my_warning =
  CWarnings.create ~name:"my-warning" ~category:"my-category"
    (fun args -> Pp.strbrk ...)

2) print it by:

warn_my_warning args
---
 interp/notation.ml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index e777e5c24..b0a219200 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -190,7 +190,8 @@ let declare_delimiters scope key =
     | None -> scope_map := String.Map.add scope newsc !scope_map
     | Some oldkey when String.equal oldkey key -> ()
     | Some oldkey ->
-	Feedback.msg_warning
+        (** FIXME: implement multikey scopes? *)
+	Flags.if_verbose Feedback.msg_info
 	  (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
 	scope_map := String.Map.add scope newsc !scope_map
   end;
@@ -198,7 +199,7 @@ let declare_delimiters scope key =
     let oldscope = String.Map.find key !delimiters_map in
     if String.equal oldscope scope then ()
     else begin
-      Feedback.msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
+      Flags.if_verbose Feedback.msg_info (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
       delimiters_map := String.Map.add key scope !delimiters_map
     end
   with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map
@@ -207,7 +208,7 @@ let remove_delimiters scope =
   let sc = find_scope scope in
   let newsc = { sc with delimiters = None } in
   match sc.delimiters with
-    | None -> Feedback.msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
+    | None -> Errors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
     | Some key ->
        scope_map := String.Map.add scope newsc !scope_map;
        try
@@ -386,6 +387,12 @@ let level_of_notation ntn =
 
 (* The mapping between notations and their interpretation *)
 
+let warn_notation_overridden =
+  CWarnings.create ~name:"notation-overridden" ~category:"parsing"
+                   (fun (ntn,which_scope) ->
+                    str "Notation" ++ spc () ++ str ntn ++ spc ()
+                    ++ strbrk "was already used" ++ which_scope)
+
 let declare_notation_interpretation ntn scopt pat df ~onlyprint =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
@@ -393,8 +400,8 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
     if String.Map.mem ntn sc.notations then
     let which_scope = match scopt with
     | None -> mt ()
-    | Some _ -> str " in scope " ++ str scope in
-    Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
+    | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
+    warn_notation_overridden (ntn,which_scope)
   in
   let notdata = {
     not_interp = pat;
-- 
cgit v1.2.3