From c9f9a159818c138af3b8d8a3a1023a66b88be207 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 18 Jun 2016 00:41:33 +0200
Subject: [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.
---
 dev/doc/changes.txt | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 4135ddd2db..4199b71418 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:
-- 
cgit v1.2.3


From 670519d2568c1a84331bd35a32b56887bb7191d9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 25 Jun 2016 16:36:20 +0200
Subject: [doc] Update changes for feedback.

I've included some other changes that didn't happen in this PR.
---
 dev/doc/changes.txt | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 4199b71418..f7c8fbb304 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -44,16 +44,24 @@ val emacs_logger    : logger
 val feedback_logger : logger
 ````
 
+* Changes in the Feedback format/Protocol.
+
+- The `Message` feedback type now carries an optional location, the main
+  payload is encoded using the richpp document format.
+
+- The `ErrorMsg` feedback type is thus unified now with `Message` at
+  level `Error`.
+
 * We now provide several loggers, `log_via_feedback` is removed in
   favor of `set_logger feedback_logger`. Output functions are:
 
 ```` ocaml
 val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-val msg_info    : Pp.std_ppcmds -> unit
-val msg_notice  : Pp.std_ppcmds -> unit
-val msg_warning : Pp.std_ppcmds -> unit
-val msg_error   : Pp.std_ppcmds -> unit
-val msg_debug   : Pp.std_ppcmds -> unit
+val msg_error   : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_notice  : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_info    : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_debug   : ?loc:Loc.t -> Pp.std_ppcmds -> unit
 ````
 
   with the `msg_*` functions being just an alias for `logger $Level`.
@@ -72,6 +80,8 @@ val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
 val get_id_for_feedback : unit -> edit_or_state_id * route_id
 ````
 
+** Kernel API changes **
+
 - The interface of the Context module was changed.
   Related types and functions were put in separate submodules.
   The mapping from old identifiers to new identifiers is the following:
-- 
cgit v1.2.3