diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-18 00:41:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-25 17:17:44 +0200 |
| commit | c9f9a159818c138af3b8d8a3a1023a66b88be207 (patch) | |
| tree | 08f3a8ecb129753981150169e50cf5dd498623d0 /toplevel | |
| parent | 9bff82239c2a6412a26ae3c5faab42a9c9d2ccb1 (diff) | |
[feedback] Add optional ?loc parameter to loggers.
This is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.
The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
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 |