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, 3 insertions, 3 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index be6ce59bd3..3fa600ac29 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -169,7 +169,7 @@ let do_daimon () =
       daimon_instr env p
     end
   in
-  if not status then Pp.feedback Feedback.AddedAxiom else ()
+  if not status then Feedback.feedback Feedback.AddedAxiom else ()
 
 (* post-instruction focus management *)
 
@@ -291,7 +291,7 @@ let justification tac gls=
 	   error "Insufficient justification."
 	 else
 	   begin
-	     msg_warning (str "Insufficient justification.");
+	     Feedback.msg_warning (str "Insufficient justification.");
 	     daimon_tac gls
 	   end) gls
 
@@ -1293,7 +1293,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	       end;
 	       match bro with
 		   None ->
-		     msg_warning (str "missing case");
+		     Feedback.msg_warning (str "missing case");
 		     tacnext (mkMeta 1)
 		 | Some (sub_ids,tree) ->
 		     let br_args =