[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.

4 files changed, 68 insertions, 34 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 2cb608326..e9506803d 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -14,8 +14,7 @@ open Vernac
 open Pcoq
 
 let top_stderr x =
-  pp_with ~pp_tag:Ppstyle.to_format !Pp_control.err_ft x;
-  Format.pp_print_flush !Pp_control.err_ft ()
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ~pp_tag:Ppstyle.to_format) x
 
 (* A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
@@ -253,7 +252,8 @@ let print_toplevel_error (e, info) =
       else mt ()
     else print_location_in_file loc
   in
-  locmsg ++ CErrors.iprint (e, info)
+  let hdr msg = hov 0 (tag Ppstyle.error_tag (str "Error:") ++ spc () ++ msg) in
+  locmsg ++ hdr (CErrors.iprint (e, info))
 
 (* Read the input stream until a dot is encountered *)
 let parse_to_dot =
@@ -285,6 +285,33 @@ let read_sentence input =
     discard_to_dot ();
     iraise reraise
 
+(** Coqloop Console feedback handler *)
+let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
+  match fb.contents with
+  | Processed   -> ()
+  | Incomplete  -> ()
+  | Complete    -> ()
+  | ProcessingIn _ -> ()
+  | InProgress _ -> ()
+  | WorkerStatus (_,_) -> ()
+  | AddedAxiom  -> ()
+  | GlobRef (_,_,_,_,_) -> ()
+  | GlobDef (_,_,_,_) -> ()
+  | FileDependency (_,_) -> ()
+  | FileLoaded (_,_) -> ()
+  | Custom (_,_,_) -> ()
+  | Message (Error,loc,msg) ->
+    (* We ignore errors here as we (still) have a different error
+       printer for the toplevel. It is hard to solve due the many
+       error paths presents, and the different compromise of feedback
+       error forwaring in the stm depending on the mode *)
+    ()
+  | Message (lvl,loc,msg) ->
+    if !Flags.print_emacs then
+      Topfmt.emacs_logger ?loc lvl msg
+    else
+      Topfmt.std_logger ?loc lvl msg
+
 (** [do_vernac] reads and executes a toplevel phrase, and print error
     messages when an exception is raised, except for the following:
     - Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
@@ -307,12 +334,13 @@ let do_vernac () =
         top_stderr (fnl ()); raise CErrors.Quit
     | CErrors.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise CErrors.Drop
-        else Feedback.msg_error (str"There is no ML toplevel.")
+        else top_stderr (str "There is no ML toplevel.")
     | any ->
+        (** Main error printer, note that this didn't it the "emacs"
+            legacy path. *)
         let any = CErrors.push any in
         let msg = print_toplevel_error any ++ fnl () in
-        pp_with !Pp_control.std_ft msg;
-        Format.pp_print_flush !Pp_control.std_ft ()
+        top_stderr msg
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -320,22 +348,13 @@ let do_vernac () =
     exit the loop are Drop and Quit. Any other exception there indicates
     an issue with [print_toplevel_error] above. *)
 
-(*
-let feed_emacs = function
-  | { Interface.id = Interface.State id;
-      Interface.content = Interface.GlobRef (_,a,_,c,_) }  -> 
-    prerr_endline ("<info>" ^"<id>"^Stateid.to_string id ^"</id>"
-		   ^a^" "^c^ "</info>")
-  | _  -> ()
-*)
-
 (* Flush in a compatible order with 8.5 *)
 (* This mimics the semantics of the old Pp.flush_all *)
 let loop_flush_all () =
   Pervasives.flush stderr;
   Pervasives.flush stdout;
-  Format.pp_print_flush !Pp_control.std_ft ();
-  Format.pp_print_flush !Pp_control.err_ft ()
+  Format.pp_print_flush !Topfmt.std_ft ();
+  Format.pp_print_flush !Topfmt.err_ft ()
 
 let rec loop () =
   Sys.catch_break true;
@@ -348,9 +367,9 @@ let rec loop () =
     | CErrors.Drop -> ()
     | CErrors.Quit -> exit 0
     | any ->
-      Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
-                str (Printexc.to_string any) ++
-                fnl() ++
-                str"Please report" ++
-                strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
+      top_stderr (str"Anomaly: main loop exited with exception: " ++
+                  str (Printexc.to_string any) ++
+                  fnl() ++
+                  str"Please report" ++
+                  strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
       loop ()
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index d248f2f70..eb61084e0 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -32,6 +32,8 @@ val set_prompt : (unit -> string) -> unit
 
 val print_toplevel_error : Exninfo.iexn -> std_ppcmds
 
+val coqloop_feed : Feedback.feedback -> unit
+
 (** Parse and execute one vernac command. *)
 
 val do_vernac : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 541c1fd1b..823d05580 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -61,7 +61,7 @@ let init_color () =
     match colors with
     | None ->
       (** Default colors *)
-      Feedback.init_color_output ()
+      Topfmt.init_color_output ()
     | Some "" ->
       (** No color output *)
       ()
@@ -69,7 +69,7 @@ let init_color () =
       (** Overwrite all colors *)
       Ppstyle.clear_styles ();
       Ppstyle.parse_config s;
-      Feedback.init_color_output ()
+      Topfmt.init_color_output ()
   end
 
 let toploop_init = ref begin fun x ->
@@ -78,15 +78,27 @@ let toploop_init = ref begin fun x ->
   x
   end
 
-let toploop_run = ref (fun () ->
+(* Feedback received in the init stage, this is different as the STM
+   will not be generally be initialized, thus stateid, etc... may be
+   bogus. For now we just print to the console too *)
+let coqtop_init_feed = Coqloop.coqloop_feed
+
+(* Default toplevel loop *)
+let console_toploop_run () =
+  (* We initialize the console only if we run the toploop_run *)
+  let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
   if Dumpglob.dump () then begin
     if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
   Coqloop.loop();
+  (* We remove the feeder but it could be ok not to do so *)
+  Feedback.del_feeder tl_feed;
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
-  Mltop.ocaml_toploop())
+  Mltop.ocaml_toploop()
+
+let toploop_run = ref console_toploop_run
 
 let output_context = ref false
 
@@ -228,7 +240,6 @@ let compile_files () =
   if !compile_list == [] then ()
   else
     let init_state = States.freeze ~marshallable:`No in
-    Feedback.(add_feeder debug_feeder);
     List.iter (fun vf ->
         States.unfreeze init_state;
         compile_file vf)
@@ -240,7 +251,6 @@ let set_emacs () =
   if not (Option.is_empty !toploop) then
     error "Flag -emacs is incompatible with a custom toplevel loop";
   Flags.print_emacs := true;
-  Feedback.(set_logger emacs_logger);
   Vernacentries.qed_display_script := false;
   color := `OFF
 
@@ -435,7 +445,7 @@ let get_native_name s =
     with the appropriate error code *)
 let fatal_error info anomaly =
   let msg = info ++ fnl () in
-  Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg;
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ?pp_tag:None) msg;
   exit (if anomaly then 129 else 1)
 
 let parse_args arglist =
@@ -609,6 +619,7 @@ let parse_args arglist =
 let init_toplevel arglist =
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
+  let init_feeder = Feedback.add_feeder coqtop_init_feed in
   Lib.init();
   begin
     try
@@ -663,7 +674,8 @@ let init_toplevel arglist =
       Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
     Profile.print_profile ();
     exit 0
-  end
+  end;
+  Feedback.del_feeder init_feeder
 
 let start () =
   let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5d17054fc..4fc4540c1 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -143,8 +143,8 @@ let pr_new_syntax_in_context loc chan_beautify ocom =
       | None -> mt() in
     let after = comment (CLexer.extract_comments (snd loc)) in
     if !beautify_file then
-      (Pp.pp_with !Pp_control.std_ft (hov 0 (before ++ com ++ after));
-       Format.pp_print_flush !Pp_control.std_ft ())
+      (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after));
+       Format.pp_print_flush !Topfmt.std_ft ())
     else
       Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
     States.unfreeze fs;
@@ -179,9 +179,10 @@ let pp_cmd_header loc com =
 (* This is a special case where we assume we are in console batch mode
    and take control of the console.
  *)
+(* FIXME *)
 let print_cmd_header loc com =
-  Pp.pp_with ~pp_tag:Ppstyle.to_format !Pp_control.std_ft (pp_cmd_header loc com);
-  Format.pp_print_flush !Pp_control.std_ft ()
+  Pp.pp_with ~pp_tag:Ppstyle.to_format !Topfmt.std_ft (pp_cmd_header loc com);
+  Format.pp_print_flush !Topfmt.std_ft ()
 
 let rec interp_vernac po chan_beautify checknav (loc,com) =
   let interp = function