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 /ide | |
| 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 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9f10b2502..b1f417757 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -472,7 +472,7 @@ let print_xml = with e -> let e = Errors.push e in Mutex.unlock m; iraise e -let slave_logger xml_oc level message = +let slave_logger xml_oc ?loc level message = (* convert the message into XML *) let msg = hov 0 message in let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in |