From ef02dca29b1bbeefc15c50e525971b425eeb05b4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 13 Sep 2016 09:39:54 +0200
Subject: coqc: print debug feedback coming from workers

This way par:eauto and all:eato print the same debugging traecs
---
 toplevel/coqtop.ml | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a56459f180..ee331e37c7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -227,18 +227,16 @@ let compile_file (v,f) =
     Vernac.compile v f
 
 let compile_files () =
-  match !compile_list with
-    | [] -> ()
-    | [vf] -> compile_file vf (* One compilation : no need to save init state *)
-    | l ->
-      let init_state = States.freeze ~marshallable:`No in
-      let coqdoc_init_state = CLexer.location_table () in
-      List.iter
-        (fun vf ->
-	  States.unfreeze init_state;
-	  CLexer.restore_location_table coqdoc_init_state;
-          compile_file vf)
-        (List.rev l)
+  if !compile_list == [] then ()
+  else
+    let init_state = States.freeze ~marshallable:`No in
+    let coqdoc_init_state = CLexer.location_table () in
+    Feedback.(add_feeder debug_feeder);
+    List.iter (fun vf ->
+        States.unfreeze init_state;
+        CLexer.restore_location_table coqdoc_init_state;
+        compile_file vf)
+      (List.rev !compile_list)
 
 (** Options for proof general *)
 
-- 
cgit v1.2.3