diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-27 15:16:56 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-27 18:35:08 +0200 |
| commit | d4725f692a5f202ca4c5d6341b586b0e377f6973 (patch) | |
| tree | 9cd74c65a51ca06547e9117b4d4901ec18a9519b /toplevel | |
| parent | 403c12ac3e8a9c3719aacbfa113600abc74846b7 (diff) | |
| parent | a10e3e0252560992128f490dfcb3d76c4bbf317b (diff) | |
Merge remote-tracking branch 'github/pr/223' into feedback-locations
Was PR#223: Allow feedback messages to carry a location.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 7d8c67025..8d20bf3d1 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -898,7 +898,7 @@ let find_precedence lev etyps symbols = | ETName | ETBigint | ETReference -> begin match lev with | None -> - ([Feedback.msg_info,strbrk "Setting notation at level 0."],0) + ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) | Some 0 -> ([],0) | _ -> @@ -916,7 +916,7 @@ let find_precedence lev etyps symbols = else [],Option.get lev) | Terminal _ when last_is_terminal () -> if Option.is_empty lev then - ([Feedback.msg_info,strbrk "Setting notation at level 0."], 0) + ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) else [],Option.get lev | _ -> if Option.is_empty lev then error "Cannot determine the level."; @@ -988,12 +988,12 @@ let compute_pure_syntax_data df mods = let (msgs,(onlyparse,onlyprint,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in let msgs = if onlyparse then - (Feedback.msg_warning, + (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, + (Feedback.msg_warning ?loc:None, strbrk "The only printing modifier has no effect in Reserved Notation.")::msgs else msgs in msgs, sy_data, extra |