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.

10 files changed, 29 insertions, 27 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 77eac9ee9..431c914c0 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -904,10 +904,10 @@ let compile fail_on_error ?universes:(universes=0) env c =
     in
     let fv = List.rev (!(reloc.in_env).fv_rev) in
     (if !Flags.dump_bytecode then
-      Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
+      Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive tname ->
-    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
+    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning in
       (Pp.(fn
 	   (str "Cannot compile code for virtual machine as it uses inductive " ++
 	    Id.print tname ++ str str_max_constructors));
diff --git a/kernel/closure.ml b/kernel/closure.ml
index bf3801e54..65123108f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -45,7 +45,7 @@ let reset () =
   prune := 0
 
 let stop() =
-  msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+  Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
 	 str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
 	 int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++
 	 str"]")
diff --git a/kernel/names.ml b/kernel/names.ml
index e8226d3d3..9abc9842a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -36,7 +36,7 @@ struct
 
   let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then Errors.error x else if warn then Pp.msg_warning (str x)
+      if fatal then Errors.error x else if warn then Feedback.msg_warning (str x)
     in
     Option.iter iter (Unicode.ident_refutation x)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 79e5d3af0..44cf21cff 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1863,7 +1863,7 @@ let compile_constant env sigma prefix ~interactive con cb =
     | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
-      if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
+      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
       let is_lazy = is_lazy prefix t in
       let code = if is_lazy then mk_lazy code else code in
       let name =
@@ -1878,11 +1878,11 @@ let compile_constant env sigma prefix ~interactive con cb =
 	  let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
           (auxdefs,mkMLlam [|univ|] code)
       in
-      if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code");
+      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code");
       let code =
         optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs)
       in
-      if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code");
+      if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
       code, name
     | _ -> 
         let i = push_symbol (SymbConst con) in
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 4ed926f1f..a0ff9e123 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -134,12 +134,12 @@ let native_conv_gen pb sigma env univs t1 t2 =
   match compile ml_filename code with
   | (true, fn) ->
       begin
-        if !Flags.debug then Pp.msg_debug (Pp.str "Running test...");
+        if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
         let t0 = Sys.time () in
         call_linker ~fatal:true prefix fn (Some upds);
         let t1 = Sys.time () in
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-        if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
         (* TODO change 0 when we can have deBruijn *)
         fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
@@ -149,7 +149,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
 let native_conv cv_pb sigma env t1 t2 =
   if Coq_config.no_native_compiler then begin
     let msg = "Native compiler is disabled, falling back to VM conversion test." in
-    Pp.msg_warning (Pp.str msg);
+    Feedback.msg_warning (Pp.str msg);
     vm_conv cv_pb env t1 t2
   end
   else
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4296b73ab..5b92e9554 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -73,20 +73,20 @@ let call_compiler ml_filename =
     ::"-w"::"a"
     ::include_dirs
     @ ["-impl"; ml_filename] in
-  if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
+  if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
   try
     let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
       | Unix.WEXITED n ->
-         Pp.(msg_warning (str "command exited with status " ++ int n)); false
+         Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false
       | Unix.WSIGNALED n ->
-         Pp.(msg_warning (str "command killed by signal " ++ int n)); false
+         Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false
       | Unix.WSTOPPED n ->
-         Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in
+         Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in
     res, link_filename
   with Unix.Unix_error (e,_,_) ->
-    Pp.(msg_warning (str (Unix.error_message e)));
+    Feedback.msg_warning Pp.(str (Unix.error_message e));
     false, link_filename
 
 let compile fn code =
@@ -120,7 +120,7 @@ let call_linker ?(fatal=true) prefix f upds =
     begin
       let msg = "Cannot find native compiler file " ^ f in
       if fatal then Errors.error msg
-      else if !Flags.debug then Pp.msg_debug (Pp.str msg)
+      else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
     end
   else
   (try
@@ -129,8 +129,8 @@ let call_linker ?(fatal=true) prefix f upds =
    with Dynlink.Error e as exn ->
      let exn = Errors.push exn in
      let msg = "Dynlink error, " ^ Dynlink.error_message e in
-     if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
-     else if !Flags.debug then Pp.msg_debug (Pp.str msg));
+     if fatal then (Feedback.msg_error (Pp.str msg); iraise exn)
+     else if !Flags.debug then Feedback.msg_debug (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 9d159be64..246b00da4 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -29,13 +29,13 @@ and translate_field prefix mp env acc (l,x) =
      let con = make_con mp empty_dirpath l in
      (if !Flags.debug then
 	let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      compile_constant_field (pre_env env) prefix con acc cb
   | SFBmind mb ->
      (if !Flags.debug then
 	let id = mb.mind_packets.(0).mind_typename in
 	let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      compile_mind_field prefix mp l acc mb
   | SFBmodule md ->
      let mp = md.mod_mp in
@@ -43,7 +43,7 @@ and translate_field prefix mp env acc (l,x) =
 	let msg =
 	  Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
 	in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env md.mod_type acc
   | SFBmodtype mdtyp ->
      let mp = mdtyp.mod_mp in
@@ -51,11 +51,11 @@ and translate_field prefix mp env acc (l,x) =
 	let msg =
 	  Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
 	in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env mdtyp.mod_type acc
 
 let dump_library mp dp env mod_expr =
-  if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
+  if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library...");
   match mod_expr with
   | NoFunctor struc ->
       let env = add_structure mp struc empty_delta_resolver env in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5bf369441..30a346c91 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -681,7 +681,7 @@ let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
-    Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
+    Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
     gen_conv cv_pb env t1 t2
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3839135a8..6bfd2457a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -167,8 +167,10 @@ let hcons_j j =
   { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
 
 let feedback_completion_typecheck =
-  Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-	      
+  let open Feedback in
+  Option.iter (fun state_id ->
+      feedback ~id:(State state_id) Feedback.Complete)
+
 let infer_declaration ~trust env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 89e833254..53db6f5be 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -185,7 +185,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
     let v2 = val_of_constr env t2 in
     fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
   with Not_found | Invalid_argument _ ->
-    (Pp.msg_warning
+    (Feedback.msg_warning
       (Pp.str "Bytecode compilation failed, falling back to default conversion");
      Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
 			    full_transparent_state env univs t1 t2)