From 10af47a5790987ee5211bac88c3a16396f30bcb0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 26 Nov 2014 18:41:34 +0100
Subject: Feedback: API cleaned up, documented and made user extensible

---
 lib/pp.ml | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'lib/pp.ml')

diff --git a/lib/pp.ml b/lib/pp.ml
index 568d80b626..405eacffe3 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -460,17 +460,20 @@ let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg
 (** Feedback *)
 
 let feeder = ref ignore
-let set_id_for_feedback ?(route=0) i = feedback_id := i; feedback_route := route
-let feedback ?state_id ?route what =
+let set_id_for_feedback ?(route=Feedback.default_route) i =
+  feedback_id := i; feedback_route := route
+let feedback ?state_id ?edit_id ?route what =
   !feeder {
-     Feedback.content = what;
+     Feedback.contents = what;
      Feedback.route = Option.default !feedback_route route;
      Feedback.id =
-       match state_id with
-       | Some id -> Feedback.State id
-       | None -> !feedback_id;
+       match state_id, edit_id with
+       | Some id, _ -> Feedback.State id
+       | None, Some eid -> Feedback.Edit eid
+       | None, None -> !feedback_id;
   }
 let set_feeder f = feeder := f
+let get_id_for_feedback () = !feedback_id, !feedback_route
 
 (** Utility *)
 
@@ -480,7 +483,7 @@ let string_of_ppcmds c =
 
 let log_via_feedback () = logger := (fun ~id lvl msg ->
   !feeder {
-     Feedback.content = Feedback.Message {
+     Feedback.contents = Feedback.Message {
        message_level = lvl;
        message_content = string_of_ppcmds msg };
      Feedback.route = !feedback_route;
-- 
cgit v1.2.3