aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-14 11:40:15 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-14 11:40:15 +0200
commit5e4dc9a1896a1dff832089be20cd43f4f4776869 (patch)
treef8661480501f26b7d3dd46e064c1a6084991a280 /lib
parent93a03345830047310d975d5de3742fa58a0a224b (diff)
parent3e794be5f02ed438cdc5a351d09bdfb54c0be01a (diff)
Merge branch 'v8.6'
Diffstat (limited to 'lib')
-rw-r--r--lib/feedback.ml5
-rw-r--r--lib/feedback.mli3
2 files changed, 8 insertions, 0 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 4bda936f2..dd1ca2af3 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -128,6 +128,11 @@ let msg_debug ?loc x = !logger ?loc Debug x
let feeders = ref []
let add_feeder f = feeders := f :: !feeders
+let debug_feeder = function
+ | { contents = Message (Debug, loc, pp) } ->
+ msg_debug ?loc (Pp.str (Richpp.raw_print pp))
+ | _ -> ()
+
let feedback_id = ref (Edit 0)
let feedback_route = ref default_route
diff --git a/lib/feedback.mli b/lib/feedback.mli
index d19517bb9..48b1c19a6 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -86,6 +86,9 @@ val emacs_logger : logger
(** [add_feeder] feeders observe the feedback *)
val add_feeder : (feedback -> unit) -> unit
+(** Prints feedback messages of kind Message(Debug,_) using msg_debug *)
+val debug_feeder : feedback -> unit
+
(** [feedback ?id ?route fb] produces feedback fb, with [route] and
[id] set appropiatedly, if absent, it will use the defaults set by
[set_id_for_feedback] *)