1 files changed, 12 insertions, 0 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 85c623f0c8..c346943e15 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -354,6 +354,18 @@ let msg_debug x = !logger (Debug "_") x
 
 let set_logger l = logger := l
 
+(** Feedback *)
+
+let feeder = ref ignore
+let feedback_id = ref 0
+let set_id_for_feedback i = feedback_id := i
+let feedback what =
+  !feeder {
+     Interface.edit_id = !feedback_id;
+     Interface.content = what
+  }
+let set_feeder f = feeder := f
+
 (** Utility *)
 
 let string_of_ppcmds c =