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.

4 files changed, 7 insertions, 6 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 5367a907e..45af036fb 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -111,7 +111,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     let () =
       match info_lvl with
       | None -> ()
-      | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+      | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
     in
     (p,status)
   with
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 681a7fa1a..caa9b328a 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -128,7 +128,7 @@ let suggest_Proof_using name env vars ids_typ context_ids =
   if S.equal all_needed fwd_typ then valid (str "Type*");
   if S.equal all all_needed then valid(str "All");
   valid (pr_set false needed);
-  msg_info (
+  Feedback.msg_info (
     str"The proof of "++ str name ++ spc() ++
     str "should start with one of the following commands:"++spc()++
     v 0 (
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 2d886b8e1..13b5848a3 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -31,7 +31,7 @@ let cbv_vm env sigma c =
 
 let cbv_native env sigma c =
   if Coq_config.no_native_compiler then
-    let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
+    let () = Feedback.msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
     cbv_vm env sigma c
   else
     let ctyp = Retyping.get_type_of env sigma c in
@@ -221,7 +221,7 @@ let reduction_of_red_expr env =
      let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
      let () =
        if not (!simplIsCbn || List.is_empty f.rConst) then
-	 Pp.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in
+	 Feedback.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in
      (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
   | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
   | Cbn f ->
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 186525e15..23433692c 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -57,7 +57,7 @@ let tclIDTAC gls = goal_goal_list gls
 
 (* the message printing identity tactic *)
 let tclIDTAC_MESSAGE s gls =
-  Pp.msg_info (hov 0 s); pp_flush (); tclIDTAC gls
+  Feedback.msg_info (hov 0 s); tclIDTAC gls
 
 (* General failure tactic *)
 let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
@@ -218,7 +218,8 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
 	   (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc)
 	   "" lh))
     "" newhyps in
-  pp (str (emacs_str "<infoH>")
+  Feedback.msg_notice
+    (str (emacs_str "<infoH>")
       ++  (hov 0 (str s))
       ++  (str (emacs_str "</infoH>")) ++ fnl());
   tclIDTAC goal;;