[pp] Make feedback the only logging mechanism.

Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.

This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.

Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.

However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.

The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.

We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.

`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.

Thus, the new panorama is:

- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
  It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
  to coqtop.

_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.

_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.

A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.

The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.

6 files changed, 320 insertions, 31 deletions

diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 5b91af03ca..f1e0c48f03 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -45,15 +45,9 @@ let _ = CErrors.register_handler explain_exn_default
 
 (** Pre-explain a vernac interpretation error *)
 
-let wrap_vernac_error with_header (exn, info) strm =
-  if with_header then
-    let header = Pp.tag Ppstyle.error_tag (str "Error:") in
-    let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
-    (e, info)
-  else
-    (EvaluatedError (strm, None), info)
+let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info)
 
-let process_vernac_interp_error with_header exn = match fst exn with
+let process_vernac_interp_error exn = match fst exn with
   | Univ.UniverseInconsistency i ->
     let msg =
       if !Constrextern.print_universes then
@@ -61,40 +55,40 @@ let process_vernac_interp_error with_header exn = match fst exn with
 	  Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
       else
 	mt() in
-    wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".")
+    wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
   | TypeError(ctx,te) ->
-      wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te)
+      wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
   | PretypeError(ctx,sigma,te) ->
-      wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te)
+      wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
-      wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te)
+      wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
   | InductiveError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_inductive_error e)
+      wrap_vernac_error exn (Himsg.explain_inductive_error e)
   | Modops.ModuleTypingError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_module_error e)
+      wrap_vernac_error exn (Himsg.explain_module_error e)
   | Modintern.ModuleInternalizationError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e)
+      wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
   | RecursionSchemeError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e)
+      wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e)
   | Cases.PatternMatchingError (env,sigma,e) ->
-      wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e)
+      wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e)
   | Tacred.ReductionTacticError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e)
+      wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_refiner_error e)
+      wrap_vernac_error exn (Himsg.explain_refiner_error e)
   | Nametab.GlobalizationError q ->
-      wrap_vernac_error with_header exn
+      wrap_vernac_error exn
         (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
 	 spc () ++ str "was not found" ++
 	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
   | Refiner.FailError (i,s) ->
       let s = Lazy.force s in
-      wrap_vernac_error with_header exn
+      wrap_vernac_error exn
 	(str "Tactic failure" ++
          (if Pp.ismt s then s else str ": " ++ s) ++
          if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
-      wrap_vernac_error with_header exn (msg ++ str ".")
+      wrap_vernac_error exn (msg ++ str ".")
   | _ ->
       exn
 
@@ -108,9 +102,9 @@ let additional_error_info = ref []
 let register_additional_error_info f =
   additional_error_info := f :: !additional_error_info
 
-let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) =
+let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
-  let e = process_vernac_interp_error with_header (exc, info) in
+  let e = process_vernac_interp_error (exc, info) in
   let () =
     if not allow_uncaught && not (CErrors.handled (fst e)) then
       let (e, info) = e in
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index a67c887af3..370ad7e3b5 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -11,7 +11,7 @@ exception EvaluatedError of Pp.std_ppcmds * exn option
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn
+val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
new file mode 100644
index 0000000000..85981c386c
--- /dev/null
+++ b/vernac/topfmt.ml
@@ -0,0 +1,245 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Feedback
+open Pp
+
+(** Pp control also belongs here as the terminal is private to the toplevel *)
+
+type pp_global_params = {
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+(* Default parameters of pretty-printing *)
+
+let dflt_gp = {
+  margin     = 78;
+  max_indent = 50;
+  max_depth  = 50;
+  ellipsis   = "..." }
+
+(* A deeper pretty-printer to print proof scripts *)
+
+let deep_gp = {
+  margin     = 78;
+  max_indent = 50;
+  max_depth  = 10000;
+  ellipsis   = "..." }
+
+(* set_gp : Format.formatter -> pp_global_params -> unit
+ * set the parameters of a formatter *)
+
+let set_gp ft gp =
+  Format.pp_set_margin ft gp.margin ;
+  Format.pp_set_max_indent ft gp.max_indent ;
+  Format.pp_set_max_boxes ft gp.max_depth ;
+  Format.pp_set_ellipsis_text ft gp.ellipsis
+
+let set_dflt_gp ft = set_gp ft dflt_gp
+
+let get_gp ft =
+  { margin = Format.pp_get_margin ft ();
+    max_indent = Format.pp_get_max_indent ft ();
+    max_depth = Format.pp_get_max_boxes ft ();
+    ellipsis = Format.pp_get_ellipsis_text ft () }
+
+(* with_fp : 'a pp_formatter_params -> Format.formatter
+ * returns of formatter for given formatter functions *)
+
+let with_fp chan out_function flush_function =
+  let ft = Format.make_formatter out_function flush_function in
+  Format.pp_set_formatter_out_channel ft chan;
+  ft
+
+(* Output on a channel ch *)
+
+let with_output_to ch =
+  let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in
+  set_gp ft deep_gp;
+  ft
+
+let std_ft = ref Format.std_formatter
+let _ = set_dflt_gp !std_ft
+
+let err_ft = ref Format.err_formatter
+let _ = set_gp !err_ft deep_gp
+
+let deep_ft = ref (with_output_to stdout)
+let _ = set_gp !deep_ft deep_gp
+
+(* For parametrization through vernacular *)
+let default = Format.pp_get_max_boxes !std_ft ()
+let default_margin = Format.pp_get_margin !std_ft ()
+
+let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ())
+let set_depth_boxes v =
+  Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v)
+
+let get_margin () = Some (Format.pp_get_margin !std_ft ())
+let set_margin v =
+  let v = match v with None -> default_margin | Some v -> v in
+  Format.pp_set_margin Format.str_formatter v;
+  Format.pp_set_margin !std_ft v;
+  Format.pp_set_margin !deep_ft v;
+  (* Heuristic, based on usage: the column on the right of max_indent
+     column is 20% of width, capped to 30 characters *)
+  let m = max (64 * v / 100) (v-30) in
+  Format.pp_set_max_indent Format.str_formatter m;
+  Format.pp_set_max_indent !std_ft m;
+  Format.pp_set_max_indent !deep_ft m
+
+(** Console display of feedback *)
+
+type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
+
+let msgnl_with ?pp_tag fmt strm =
+  pp_with ?pp_tag fmt (strm ++ fnl ());
+  Format.pp_print_flush fmt ()
+
+(* XXX: This is really painful! *)
+module Emacs = struct
+
+  (* Special chars for emacs, to detect warnings inside goal output *)
+  let emacs_quote_start = String.make 1 (Char.chr 254)
+  let emacs_quote_end   = String.make 1 (Char.chr 255)
+
+  let emacs_quote_err g =
+    hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
+
+  let emacs_quote_info_start = "<infomsg>"
+  let emacs_quote_info_end = "</infomsg>"
+
+  let emacs_quote_info g =
+    hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
+
+end
+
+open Emacs
+
+let  dbg_str = tag Ppstyle.debug_tag   (str "Debug:")   ++ spc ()
+let info_str = mt ()
+let warn_str = tag Ppstyle.warning_tag (str "Warning:") ++ spc ()
+let  err_str = tag Ppstyle.error_tag   (str "Error:")   ++ spc ()
+
+let make_body quoter info ?loc s =
+  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
+  quoter (hov 0 (loc ++ info ++ s))
+
+(* Generic logger *)
+let gen_logger ?pp_tag dbg err ?loc level msg = match level with
+  | Debug   -> msgnl_with ?pp_tag !std_ft (make_body dbg  dbg_str ?loc msg)
+  | Info    -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg)
+  (* XXX: What to do with loc here? *)
+  | Notice  -> msgnl_with ?pp_tag !std_ft msg
+  | Warning -> Flags.if_warn (fun () ->
+               msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) ()
+  | Error   -> msgnl_with ?pp_tag !err_ft (make_body err  err_str ?loc msg)
+
+(** Standard loggers *)
+
+(* We provide a generic clear_log_backend callback for backends
+   wanting to do clenaup after the print.
+*)
+let std_logger_tag     = ref None
+let std_logger_cleanup = ref (fun () -> ())
+
+let std_logger ?loc level msg =
+  gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg;
+  !std_logger_cleanup ()
+
+(** Color logging. Moved from pp_style, it may need some more refactoring  *)
+
+(** Not thread-safe. We should put a lock somewhere if we print from
+    different threads. Do we? *)
+let make_style_stack () =
+  (** Default tag is to reset everything *)
+  let empty = Terminal.make () in
+  let default_tag = Terminal.({
+      fg_color = Some `DEFAULT;
+      bg_color = Some `DEFAULT;
+      bold = Some false;
+      italic = Some false;
+      underline = Some false;
+      negative = Some false;
+    })
+  in
+  let style_stack = ref [] in
+  let peek () = match !style_stack with
+  | []      -> default_tag  (** Anomalous case, but for robustness *)
+  | st :: _ -> st
+  in
+  let push tag =
+    let style = match Ppstyle.get_style_format tag with
+      | None    -> empty
+      | Some st -> st
+    in
+    (** Use the merging of the latest tag and the one being currently pushed.
+    This may be useful if for instance the latest tag changes the background and
+    the current one the foreground, so that the two effects are additioned. *)
+    let style = Terminal.merge (peek ()) style in
+    style_stack := style :: !style_stack;
+    Terminal.eval style
+  in
+  let pop _ = match !style_stack with
+  | []       -> (** Something went wrong, we fallback *)
+                Terminal.eval default_tag
+  | _ :: rem -> style_stack := rem;
+                Terminal.eval (peek ())
+  in
+  let clear () = style_stack := [] in
+  push, pop, clear
+
+let init_color_output () =
+  let push_tag, pop_tag, clear_tag = make_style_stack () in
+  std_logger_cleanup := clear_tag;
+  std_logger_tag     := Some Ppstyle.to_format;
+  let tag_handler = {
+    Format.mark_open_tag   = push_tag;
+    Format.mark_close_tag  = pop_tag;
+    Format.print_open_tag  = ignore;
+    Format.print_close_tag = ignore;
+  } in
+  Format.pp_set_mark_tags !std_ft true;
+  Format.pp_set_mark_tags !err_ft true;
+  Format.pp_set_formatter_tag_functions !std_ft tag_handler;
+  Format.pp_set_formatter_tag_functions !err_ft tag_handler
+
+(* Rules for emacs:
+   - Debug/info: emacs_quote_info
+   - Warning/Error: emacs_quote_err
+   - Notice: unquoted
+ *)
+let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+
+(* Output to file, used only in extraction so a candidate for removal *)
+let ft_logger old_logger ft ?loc level mesg =
+  let id x = x in
+  match level with
+  | Debug   -> msgnl_with ft (make_body id  dbg_str mesg)
+  | Info    -> msgnl_with ft (make_body id info_str mesg)
+  | Notice  -> msgnl_with ft mesg
+  | Warning -> old_logger ?loc level mesg
+  | Error   -> old_logger ?loc level mesg
+
+let with_output_to_file fname func input =
+  (* XXX FIXME: redirect std_ft  *)
+  (* let old_logger = !logger in *)
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *)
+  try
+    let output = func input in
+    (* logger := old_logger; *)
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    (* logger := old_logger; *)
+    close_out channel;
+    Exninfo.iraise reraise
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
new file mode 100644
index 0000000000..38a400cfd0
--- /dev/null
+++ b/vernac/topfmt.mli
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Console printing options *)
+
+type pp_global_params = {
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+val dflt_gp : pp_global_params
+val deep_gp : pp_global_params
+val set_gp : Format.formatter -> pp_global_params -> unit
+val set_dflt_gp : Format.formatter -> unit
+val get_gp : Format.formatter -> pp_global_params
+
+(** {6 Output functions of pretty-printing. } *)
+
+val with_output_to : out_channel -> Format.formatter
+
+val std_ft  : Format.formatter ref
+val err_ft  : Format.formatter ref
+val deep_ft : Format.formatter ref
+
+(** {6 For parametrization through vernacular. } *)
+
+val set_depth_boxes : int option -> unit
+val get_depth_boxes : unit -> int option
+
+val set_margin : int option -> unit
+val get_margin : unit -> int option
+
+(** Console display of feedback *)
+val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
+
+val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
+
+val init_color_output : unit -> unit
+
+(** [with_output_to_file file f x] executes [f x] with logging
+    redirected to a file [file] *)
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 94ef54f70f..283c095eb6 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -14,4 +14,5 @@ Record
 Assumptions
 Vernacinterp
 Mltop
+Topfmt
 Vernacentries
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3afe04b37b..09c43f93ef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1448,8 +1448,8 @@ let _ =
       optdepr  = false;
       optname  = "the printing depth";
       optkey   = ["Printing";"Depth"];
-      optread  = Pp_control.get_depth_boxes;
-      optwrite = Pp_control.set_depth_boxes }
+      optread  = Topfmt.get_depth_boxes;
+      optwrite = Topfmt.set_depth_boxes }
 
 let _ =
   declare_int_option
@@ -1457,8 +1457,8 @@ let _ =
       optdepr  = false;
       optname  = "the printing width";
       optkey   = ["Printing";"Width"];
-      optread  = Pp_control.get_margin;
-      optwrite = Pp_control.set_margin }
+      optread  = Topfmt.get_margin;
+      optwrite = Topfmt.set_margin }
 
 let _ =
   declare_bool_option
@@ -2193,7 +2193,7 @@ let with_fail b f =
            | e ->
               let e = CErrors.push e in
               raise (HasFailed (CErrors.iprint
-                (ExplainErr.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e))))
+                (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))))
         ()
     with e when CErrors.noncritical e ->
       let (e, _) = CErrors.push e in
@@ -2226,7 +2226,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
     | VernacRedirect (s, (_,v)) ->
-         Feedback.with_output_to_file s (aux false) v
+         Topfmt.with_output_to_file s (aux false) v
     | VernacTime (_,v) ->
         System.with_time !Flags.time
           (aux ?locality ?polymorphism isprogcmd) v;