This patch splits pretty printing representation from IO operations.

8 files changed, 23 insertions, 23 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 879145c2fa..52094cf085 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -52,17 +52,17 @@ let rec print_debug_queue e =
       let _ =
 	match e with
 	| Some e ->
-	   Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+	   Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
 	| None ->
 	   begin
-	     Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
+	     Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
 	   end in
       print_debug_queue None ;
     end
 
 let observe strm =
   if do_observe ()
-  then Pp.msg_debug strm
+  then Feedback.msg_debug strm
   else ()
 
 let do_observe_tac s tac g = 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 91a826c731..5b4fb25955 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -19,7 +19,7 @@ exception Toberemoved
 
 let observe s =
   if do_observe ()
-  then Pp.msg_debug s
+  then Feedback.msg_debug s
 
 (*
    Transform an inductive induction principle into
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6dfc23511e..c63527deaf 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -193,12 +193,12 @@ let warning_error names e =
   let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
-	Pp.msg_warning
+	Feedback.msg_warning
 	  (str "Cannot define graph(s) for " ++
 	     h 1 (pr_enum Libnames.pr_reference names) ++
 	     if do_observe () then (spc () ++ Errors.print e) else mt ())
     | Defining_principle e ->
-	Pp.msg_warning
+	Feedback.msg_warning
 	  (str "Cannot define principle(s) for "++
 	     h 1 (pr_enum Libnames.pr_reference names) ++
 	     if do_observe () then Errors.print e else mt ())
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8a0a1a064d..72205e2bbc 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -14,7 +14,7 @@ open Misctypes
 
 let observe strm =
   if do_observe ()
-  then Pp.msg_debug strm
+  then Feedback.msg_debug strm
   else ()
 (*let observennl strm =
   if do_observe ()
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 84a4d910ef..0cacb003d8 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -267,12 +267,12 @@ let derive_inversion fix_names =
 	lind;
       with e when Errors.noncritical e ->
       let e' = process_vernac_interp_error e in
-      msg_warning
+      Feedback.msg_warning
 	(str "Cannot build inversion information" ++
 	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
   with e when Errors.noncritical e ->
       let e' = process_vernac_interp_error e in
-      msg_warning
+      Feedback.msg_warning
 	(str "Cannot build inversion information (early)" ++
 	   if do_observe () then (fnl() ++ Errors.print e') else mt ())       
 
@@ -292,12 +292,12 @@ let warning_error names e =
   in
   match e with
     | Building_graph e ->
-      Pp.msg_warning
+      Feedback.msg_warning
 	(str "Cannot define graph(s) for " ++
 	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	   e_explain e)
     | Defining_principle e ->
-      Pp.msg_warning
+      Feedback.msg_warning
 	(str "Cannot define principle(s) for "++
 	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	   e_explain e)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 72529fbbe3..94530bfde2 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -53,7 +53,7 @@ let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds =
 
 let observe strm =
   if do_observe ()
-  then Pp.msg_debug strm
+  then Feedback.msg_debug strm
   else ()
 
 (*let observennl strm =
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index c71d9a9ca4..99a165044c 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -504,19 +504,19 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
   match c1 , c2 with
     | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
-        let _ = prstr "\nICI1!\n";Pp.flush_all() in
+        let _ = prstr "\nICI1!\n" in
         let args = filter_shift_stable lnk (arr1 @ arr2) in
         GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args)
     | GApp(_,f1, arr1), GApp(_,f2,arr2)  -> raise NoMerge
     | GLetIn(_,nme,bdy,trm) , _ ->
-        let _ = prstr "\nICI2!\n";Pp.flush_all() in
+        let _ = prstr "\nICI2!\n" in
         let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
         GLetIn(Loc.ghost,nme,bdy,newtrm)
     | _, GLetIn(_,nme,bdy,trm) ->
-        let _ = prstr "\nICI3!\n";Pp.flush_all() in
+        let _ = prstr "\nICI3!\n" in
         let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
         GLetIn(Loc.ghost,nme,bdy,newtrm)
-    | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in
+    | _ -> let _ = prstr "\nICI4!\n" in
            raise NoMerge
 
 let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
@@ -527,14 +527,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
         GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args)
           (* FIXME: what if the function appears in the body of the let? *)
     | GLetIn(_,nme,bdy,trm) , _ ->
-        let _ = prstr "\nICI2 '!\n";Pp.flush_all() in
+      let _ = prstr "\nICI2 '!\n" in
         let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
         GLetIn(Loc.ghost,nme,bdy,newtrm)
     | _, GLetIn(_,nme,bdy,trm) ->
-        let _ = prstr "\nICI3 '!\n";Pp.flush_all() in
+        let _ = prstr "\nICI3 '!\n" in
         let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
         GLetIn(Loc.ghost,nme,bdy,newtrm)
-    | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge
+    | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
 
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 10f08d3d13..80866e8b8c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -214,17 +214,17 @@ let print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in 
       if b then 
-	Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+	Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
       else
 	begin
-	  Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
+	  Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
 	end;
       (* print_debug_queue false e; *)
     end
 
 let observe strm =
   if do_observe ()
-  then Pp.msg_debug strm
+  then Feedback.msg_debug strm
   else ()
 
 
@@ -1537,7 +1537,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       with e when Errors.noncritical e ->
 	begin
 	  if do_observe ()
-	  then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
+	  then Feedback.msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
 	  else anomaly (Pp.str "Cannot create equation Lemma")
 	  ;
 	  true