diff options
| author | bertot | 2001-04-04 13:32:29 +0000 |
|---|---|---|
| committer | bertot | 2001-04-04 13:32:29 +0000 |
| commit | 67109f1b472fdbc31a2c62472cef71efa8432cf8 (patch) | |
| tree | e6ba09d2bad73cb3e62a418e207d0c7898e5e9ef | |
| parent | d9765c49bd60bedb3071188aa4406c241813553e (diff) | |
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
| -rw-r--r-- | parsing/esyntax.ml | 5 | ||||
| -rw-r--r-- | parsing/esyntax.mli | 1 |
2 files changed, 5 insertions, 1 deletions
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 *) |