From 0e07e69dae3f3f4a99f824533f54a3991aacac6a Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Tue, 28 Jun 2016 13:55:20 +0200
Subject: Revert "A new infrastructure for warnings."

This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.

I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.
---
 toplevel/metasyntax.ml | 30 +++++++++---------------------
 1 file changed, 9 insertions(+), 21 deletions(-)

(limited to 'toplevel/metasyntax.ml')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index aa6601a7d..e772ea020 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -864,23 +864,16 @@ let check_rule_productivity l =
   if (match l with SProdList _ :: _ -> true | _ -> false) then
     error "A recursive notation must start with at least one symbol."
 
-let warn_notation_bound_to_variable =
-  CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing"
-         (fun () ->
-          strbrk "This notation will not be used for printing as it is bound to a single variable.")
-
-let warn_non_reversible_notation =
-  CWarnings.create ~name:"non-reversible-notation" ~category:"parsing"
-         (fun () ->
-          strbrk "This notation will not be used for printing as it is not reversible.")
-
 let is_not_printable onlyparse noninjective = function
 | NVar _ ->
-  if not onlyparse then warn_notation_bound_to_variable ();
+  let () = if not onlyparse then
+    Feedback.msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
+  in
   true
 | _ ->
-   if not onlyparse && noninjective then
-     (warn_non_reversible_notation (); true)
+  if not onlyparse && noninjective then
+    let () = Feedback.msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
+    true
   else onlyparse
 
 let find_precedence lev etyps symbols =
@@ -935,10 +928,6 @@ let check_curly_brackets_notation_exists () =
     error "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved."
 
-let warn_skip_spaces_curly =
-  CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing"
-      (fun () ->strbrk "Skipping spaces inside curly brackets")
-
 (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *)
 let remove_curly_brackets l =
   let rec skip_break acc = function
@@ -953,10 +942,9 @@ let remove_curly_brackets l =
             let br',next' = skip_break [] l' in
             (match next' with
               | Terminal "}" as t2 :: l'' as l1 ->
-                 if not (List.equal Notation.symbol_eq l l0) ||
-		      not (List.equal Notation.symbol_eq l' l1) then
-		  warn_skip_spaces_curly ();
-		  if deb && List.is_empty l'' then [t1;x;t2] else begin
+                  if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then
+                    Feedback.msg_warning (strbrk "Skipping spaces inside curly brackets");
+                  if deb && List.is_empty l'' then [t1;x;t2] else begin
                     check_curly_brackets_notation_exists ();
                     x :: aux false l''
                   end
-- 
cgit v1.2.3