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 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 4135ddd2d..4199b7141 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -30,6 +30,9 @@ val message : string -> unit proper `Feedback.msg_*` function. Clients also have no control over flushing, the back end takes care of it. + Also, the `msg_*` functions now take an optional `?loc` parameter + for relaying location to the client. + * Feedback related functions and definitions have been moved to the `Feedback` module. `message_level` has been renamed to level. Functions moved from Pp to Feedback are: |