diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-28 01:02:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-28 01:19:46 +0200 |
| commit | 97e6e937433d52eba1ab01863d19db8bd85f2bc3 (patch) | |
| tree | c72696e2aa27d3500f9bb8f144a4dd2a8cd5b629 /toplevel | |
| parent | 64e7be2e88f01ad65928e4b2b537e60c2c4e9260 (diff) | |
Properly handle the only printing flag in Reserved Notations.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 586d9f1cf..e772ea020 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -991,12 +991,7 @@ let compute_pure_syntax_data df mods = (Feedback.msg_warning ?loc:None, strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs else msgs in - let msgs = - if onlyprint then - (Feedback.msg_warning ?loc:None, - strbrk "The only printing modifier has no effect in Reserved Notation.")::msgs - else msgs in - msgs, sy_data, extra + msgs, sy_data, extra, onlyprint (**********************************************************************) (* Registration of notations interpretation *) @@ -1213,8 +1208,8 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) (* Notations without interpretation (Reserved Notation) *) let add_syntax_extension local ((loc,df),mods) = - let msgs, sy_data, extra = compute_pure_syntax_data df mods in - let sy_rules = make_syntax_rules sy_data extra false in + let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in + let sy_rules = make_syntax_rules sy_data extra onlyprint in Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) |