From 67109f1b472fdbc31a2c62472cef71efa8432cf8 Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 4 Apr 2001 13:32:29 +0000
Subject: Add a flag to avoid sending too many warnings when reloading syntax
 files in the parser used for the graphical user-interface.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1541 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/esyntax.ml  | 5 ++++-
 parsing/esyntax.mli | 1 +
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 250000b74c..64f7d877e6 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -30,6 +30,8 @@ type key =
   | Oth                (* key for other syntax rules *)
   | All     (* key for catch-all rules (i.e. with a pattern such as $x .. *)
 
+let warning_verbose = ref true
+
 let ast_keys = function
   | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl,_)]) ::_) ->
       [Cst sl; Nod "APPLIST"; All]
@@ -96,7 +98,8 @@ let remove_with_warning name =
   if Gmap.mem name !from_name_table then begin
     let se = Gmap.find name !from_name_table in
     let key = (fst name, se_key se) in
-    warning ("overriding syntax rule "^(fst name)^":"^(snd name)^".");
+      (if !warning_verbose then
+    	warning ("overriding syntax rule "^(fst name)^":"^(snd name)^"."));
     from_name_table := Gmap.remove name !from_name_table;
     from_key_table := Gmapl.remove key se !from_key_table
   end
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
index 8f7fbce75a..40c541889e 100644
--- a/parsing/esyntax.mli
+++ b/parsing/esyntax.mli
@@ -27,6 +27,7 @@ val find_syntax_entry :
   string -> Coqast.t -> (syntax_entry * Ast.env) option
 val add_rule : string -> syntax_entry -> unit
 val add_ppobject : syntax_command -> unit
+val warning_verbose : bool ref
 
 (* Pretty-printing *)
 
-- 
cgit v1.2.3