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.

9 files changed, 34 insertions, 32 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 3a5c91217..93eb2a0d2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -111,15 +111,14 @@ let check_one_lib admit (dir,m) =
      also check if it carries a validation certificate (yet to
      be implemented). *)
   if LibrarySet.mem dir admit then
-    (Flags.if_verbose ppnl
+    (Flags.if_verbose Feedback.msg_notice
       (str "Admitting library: " ++ pr_dirpath dir);
       Safe_typing.unsafe_import file md m.library_extra_univs dig)
   else
-    (Flags.if_verbose ppnl
+    (Flags.if_verbose Feedback.msg_notice
       (str "Checking library: " ++ pr_dirpath dir);
       Safe_typing.import file md m.library_extra_univs dig);
-  Flags.if_verbose pp (fnl());
-  pp_flush ();
+  Flags.if_verbose Feedback.msg_notice (fnl());
   register_loaded_library m
 
 (*************************************************************************)
@@ -173,7 +172,7 @@ let remove_load_path dir =
 
 let add_load_path (phys_path,coq_path) =
   if !Flags.debug then
-    ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+    Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
   let phys_path = canonical_path_name phys_path in
   let physical, logical = !load_paths in
@@ -188,7 +187,7 @@ let add_load_path (phys_path,coq_path) =
 	    begin
               (* Assume the user is concerned by library naming *)
 	      if dir <> default_root_prefix then
-		msg_warning
+		Feedback.msg_warning
 		  (str phys_path ++ strbrk " was previously bound to " ++
 		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
 		   pr_dirpath coq_path);
@@ -299,7 +298,7 @@ let name_clash_message dir mdir f =
 let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
-  Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
+  Flags.if_verbose Feedback.msg_notice(str"[intern "++str f++str" ...");
   let (sd,md,table,opaque_csts,digest) =
     try
       let ch = System.with_magic_number_check raw_intern_library f in
@@ -323,7 +322,7 @@ let intern_from_file (dir, f) =
         errorlabstrm "intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
-        pp (str " (was a vio file) ");
+       Feedback.msg_notice(str " (was a vio file) ");
       Option.iter (fun (_,_,b) -> if not b then
         errorlabstrm "intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
@@ -334,12 +333,12 @@ let intern_from_file (dir, f) =
       Validate.validate !Flags.debug Values.v_libsum sd;
       Validate.validate !Flags.debug Values.v_lib md;
       Validate.validate !Flags.debug Values.v_opaques table;
-      Flags.if_verbose ppnl (str" done]"); pp_flush ();
+      Flags.if_verbose Feedback.msg_notice (str" done]");
       let digest =
         if opaque_csts <> None then Cic.Dviovo (digest,udg)
         else (Cic.Dvo digest) in
       sd,md,table,opaque_csts,digest
-    with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
+    with e -> Flags.if_verbose Feedback.msg_notice (str" failed!]"); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
   opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
   Option.iter (fun (opaque_csts,_,_) ->
@@ -407,11 +406,11 @@ let recheck_library ~norec ~admit ~check =
   let nochk =
     List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
   (* *)
-  Flags.if_verbose ppnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
+  Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
   List.iter (check_one_lib nochk) needed;
-  Flags.if_verbose ppnl (str"Modules were successfully checked")
+  Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked")
 
 open Printf
 
diff --git a/checker/check.mllib b/checker/check.mllib
index 900cfe0c8..a093fd959 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -22,16 +22,18 @@ CList
 CString
 Serialize
 Stateid
-Feedback
-Pp
-Segmenttree
-Unicodetable
-Unicode
 CObj
 CArray
 CStack
 Util
+Pp
 Ppstyle
+Xml_datatype
+Richpp
+Feedback
+Segmenttree
+Unicodetable
+Unicode
 Errors
 CEphemeron
 Future
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 84f5684d4..a26c93a30 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -57,12 +57,13 @@ let print_context env =
          env_modules=mods; env_modtypes=mtys};
        env_stratification=
         {env_universes=univ; env_engagement=engt}} = env in
-    ppnl(hov 0
+    Feedback.msg_notice
+      (hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
-      fnl())); pp_flush()
+       fnl()));
   end
 
 let stats () =
diff --git a/checker/checker.ml b/checker/checker.ml
index 91a207a60..61b13c60b 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -17,7 +17,7 @@ open Check
 let () = at_exit flush_all
 
 let fatal_error info anomaly =
-  flush_all (); pperrnl info; flush_all ();
+  flush_all (); Feedback.msg_error info; flush_all ();
   exit (if anomaly then 129 else 1)
 
 let coq_root = Id.of_string "Coq"
@@ -67,12 +67,12 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
       Check.add_load_path (dir,coq_dirpath)
     end
   else
-    msg_warning (str "Cannot open " ++ str dir)
+    Feedback.msg_warning (str "Cannot open " ++ str dir)
 
 let convert_string d =
   try Id.of_string d
   with Errors.UserError _ ->
-    if_verbose msg_warning
+    if_verbose Feedback.msg_warning
       (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
@@ -90,7 +90,7 @@ let add_rec_path ~unix_path ~coq_root =
     List.iter Check.add_load_path dirs;
     Check.add_load_path (unix_path, coq_root)
   else
-    msg_warning (str "Cannot open " ++ str unix_path)
+    Feedback.msg_warning (str "Cannot open " ++ str unix_path)
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -123,7 +123,7 @@ let init_load_path () =
     add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
   (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix)
-    (xdg_dirs ~warn:(fun x -> msg_warning (str x)));
+    (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)));
   (* then directories in COQPATH *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
   (* then current directory *)
@@ -288,7 +288,7 @@ let rec explain_exn = function
           Format.printf "@\nis not convertible with@\n";
           Print.print_pure_constr a;
           Format.printf "@\n====== universes ====@\n";
-          Pp.pp (Univ.pr_universes
+          Feedback.msg_notice (Univ.pr_universes
             (ctx.Environ.env_stratification.Environ.env_universes));
           str "\nCantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
diff --git a/checker/closure.ml b/checker/closure.ml
index c2708e97d..cef1d31a6 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -29,7 +29,7 @@ let reset () =
   beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; 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" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++
          str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]")
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index fd5eaeb8b..a667bb8a3 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -528,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds =
 (************************************************************************)
 
 let check_inductive env kn mib =
-  Flags.if_verbose ppnl (str "  checking ind: " ++ MutInd.print kn); pp_flush ();
+  Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
   (* check mind_constraints: should be consistent with env *)
   let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index c07a35e35..7f93e1560 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,7 +26,7 @@ let refresh_arity ar =
     | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
-  Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn); pp_flush ();
+  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
   let env' =
     if cb.const_polymorphic then
       let inst = Univ.make_abstract_instance cb.const_universes in
diff --git a/checker/print.ml b/checker/print.ml
index da8a6106f..c0d1ac368 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -10,7 +10,7 @@ open Format
 open Cic
 open Names
 
-let print_instance i = Pp.pp (Univ.Instance.pr i)
+let print_instance i = Feedback.msg_notice (Univ.Instance.pr i)
 
 let print_pure_constr csr =
   let rec term_display c = match  c with
@@ -108,7 +108,7 @@ let print_pure_constr csr =
   and sort_display = function
     | Prop(Pos) -> print_string "Set"
     | Prop(Null) -> print_string "Prop"
-    | Type u -> print_string "Type("; Pp.pp (Univ.pr_uni u); print_string ")"
+    | Type u -> print_string "Type("; Feedback.msg_notice (Univ.pr_uni u); print_string ")"
 
   and name_display = function
     | Name id -> print_string (Id.to_string id)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 7f9ed92f9..1071e2f93 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -81,7 +81,7 @@ let stamp_library file digest = ()
    warning is issued in case of mismatch *)
 let import file clib univs digest =
   let env = !genv in
-  check_imports msg_warning clib.comp_name env clib.comp_deps;
+  check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   let mb = clib.comp_mod in
   Mod_checking.check_module
@@ -93,7 +93,7 @@ let import file clib univs digest =
 (* When the module is admitted, digests *must* match *)
 let unsafe_import file clib univs digest =
   let env = !genv in
-  if !Flags.debug then check_imports msg_warning clib.comp_name env clib.comp_deps
+  if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps
   else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   full_add_module clib.comp_name clib.comp_mod univs digest