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

diff --git a/library/goptions.ml b/library/goptions.ml
index 5f6512e11..4aa3a2a21 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -108,7 +108,8 @@ module MakeTable =
          (fun c -> t := MySet.remove c !t))
 
     let print_table table_name printer table =
-      pp (str table_name ++
+      Feedback.msg_notice
+        (str table_name ++
 	   (hov 0
 	      (if MySet.is_empty table then str " None" ++ fnl ()
                else MySet.fold
@@ -122,7 +123,7 @@ module MakeTable =
       method mem x =
 	let y = A.encode x in
         let answer = MySet.mem y !t in
-        msg_info (A.member_message y answer)
+        Feedback.msg_info (A.member_message y answer)
       method print = print_table A.title A.printer !t
     end
 
@@ -271,7 +272,7 @@ let declare_option cast uncast
   in
   let warn () =
     if depr then
-      msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
+      Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
   in
   let cread () = cast (read ()) in
   let cwrite v = warn (); write (uncast v) in
@@ -346,12 +347,12 @@ let set_int_option_value_gen locality =
   set_option_value locality check_int_value
 let set_bool_option_value_gen locality key v =
   try set_option_value locality check_bool_value key v
-  with UserError (_,s) -> msg_warning s
+  with UserError (_,s) -> Feedback.msg_warning s
 let set_string_option_value_gen locality =
   set_option_value locality check_string_value
 let unset_option_value_gen locality key =
   try set_option_value locality check_unset_value key ()
-  with UserError (_,s) -> msg_warning s
+  with UserError (_,s) -> Feedback.msg_warning s
 
 let set_int_option_value = set_int_option_value_gen None
 let set_bool_option_value = set_bool_option_value_gen None
@@ -375,9 +376,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+	Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
     | _ ->
-	msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+	Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
 
 let get_tables () =
   let tables = !value_tab in