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