Feedback cleanup

This patch splits pretty printing representation from IO operations.

- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.

The patch continues work initiated for 8.5 and has the following effects:

- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
  `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
  `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
  used instead.

- Feedback provides different backends to handle output, currently,
  `stdout`, `emacs` and CoqIDE backends are provided.

- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
  gone.

- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
  mix.

Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.

1 files changed, 7 insertions, 7 deletions

diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index c71d9a9ca..99a165044 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