This patch splits pretty printing representation from IO operations.

4 files changed, 75 insertions, 10 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2f631c6338..53497ff0e5 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,69 @@
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
+** Logging and Pretty Printing: **
+
+* Printing functions have been removed from `Pp.mli`, which is now a
+  purely pretty-printing interface. Functions affected are:
+
+```` ocaml
+val pp          : std_ppcmds -> unit
+val ppnl        : std_ppcmds -> unit
+val pperr       : std_ppcmds -> unit
+val pperrnl     : std_ppcmds -> unit
+val pperr_flush : unit -> unit
+val pp_flush    : unit -> unit
+val flush_all   : unit -> unit
+val msg         : std_ppcmds -> unit
+val msgnl       : std_ppcmds -> unit
+val msgerr      : std_ppcmds -> unit
+val msgerrnl    : std_ppcmds -> unit
+val message     : string -> unit
+````
+
+  which are no more available. Users of `Pp.pp msg` should now use the
+  proper `Feedback.msg_*` function. Clients also have no control over
+  flushing, the back end takes care of it.
+
+* Feedback related functions and definitions have been moved to the
+  `Feedback` module. `message_level` has been renamed to
+  level. Functions moved from Pp to Feedback are:
+
+```` ocaml
+val set_logger      : logger -> unit
+val std_logger      : logger
+val emacs_logger    : logger
+val feedback_logger : logger
+````
+
+* We now provide several loggers, `log_via_feedback` is removed in
+  favor of `set_logger feedback_logger`. Output functions are:
+
+```` ocaml
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+val msg_info    : Pp.std_ppcmds -> unit
+val msg_notice  : Pp.std_ppcmds -> unit
+val msg_warning : Pp.std_ppcmds -> unit
+val msg_error   : Pp.std_ppcmds -> unit
+val msg_debug   : Pp.std_ppcmds -> unit
+````
+
+  with the `msg_*` functions being just an alias for `logger $Level`.
+
+* The main feedback functions are:
+
+```` ocaml
+val set_feeder : (feedback -> unit) -> unit
+val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+````
+  Note that `feedback` doesn't take two parameters anymore. After
+  refactoring the following function has been removed:
+
+```` ocaml
+val get_id_for_feedback : unit -> edit_or_state_id * route_id
+````
+
 - The interface of the Context module was changed.
   Related types and functions were put in separate submodules.
   The mapping from old identifiers to new identifiers is the following:
diff --git a/dev/printers.mllib b/dev/printers.mllib
index aa74cb5085..0957197cc2 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -26,16 +26,17 @@ Control
 Loc
 Serialize
 Stateid
-Feedback
-Pp
-Segmenttree
-Unicodetable
-Unicode
 CObj
 CArray
 CStack
 Util
+Pp
 Ppstyle
+Richpp
+Feedback
+Segmenttree
+Unicodetable
+Unicode
 Errors
 Bigint
 CUnix
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f5599d793f..4da901e531 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -29,7 +29,8 @@ let _ = set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
 (* std_ppcmds *)
-let pppp x = pp x
+let pp   x = Feedback.msg_notice x
+let pppp x = Feedback.msg_notice x
 
 (** Future printer *)
 
@@ -315,7 +316,7 @@ let constr_display csr =
     | Anonymous -> "Anonymous"
 
   in
-  Pp.pp (str (term_display csr) ++fnl ()); Pp.pp_flush ()
+  Feedback.msg_notice (str (term_display csr) ++fnl ())
 
 open Format;;
 
@@ -515,7 +516,7 @@ let _ =
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Pp.pp (Errors.print e)
+    e -> Feedback.msg_notice (Errors.print e)
 let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
@@ -531,7 +532,7 @@ let _ =
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Pp.pp (Errors.print e)
+    e -> Feedback.msg_notice (Errors.print e)
 let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 1c501df808..afa94a63e0 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -79,7 +79,7 @@ and ppwhd whd =
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s
-  | Vuniv_level lvl -> Pp.pp (Univ.Level.pr lvl)
+  | Vuniv_level lvl -> Feedback.msg_notice (Univ.Level.pr lvl)
 
 and ppvblock b =
   open_hbox();