aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-17 15:38:49 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-17 15:38:49 +0200
commitc852523c11ca2d5edca6f35b12557e2d09dac1d6 (patch)
tree269f75802e5d3b8a8d1001e560eea7d092a5bbed /toplevel/metasyntax.ml
parentb1b8243b7fc0bd8e2b9db3ddb28941646b3bd1ff (diff)
Now printing "now a keyword" only in verbose mode.
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r--toplevel/metasyntax.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 905df5f2b..09d4bff43 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -686,7 +686,7 @@ let is_not_small_constr = function
let rec define_keywords_aux = function
| GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
when is_not_small_constr e ->
- msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+ Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
Lexer.add_keyword k;
n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| n :: l -> n :: define_keywords_aux l
@@ -695,7 +695,7 @@ let rec define_keywords_aux = function
(* Ensure that IDENT articulation terminal symbols are keywords *)
let define_keywords = function
| GramConstrTerminal(IDENT k)::l ->
- msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+ Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
Lexer.add_keyword k;
GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| l -> define_keywords_aux l