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

1 files changed, 24 insertions, 20 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 0f3629c8f..7982ffc8b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -162,13 +162,16 @@ let flags_to_color f =
   else if List.mem `INCOMPLETE f then `NAME "gray"
   else `NAME Preferences.processed_color#get
 
-let validate s =
-  let open Xml_datatype in
-  let rec validate = function
-  | PCData s -> Glib.Utf8.validate s
-  | Element (_, _, children) -> List.for_all validate children
-  in
-  validate (Richpp.repr s)
+(* Move to utils? *)
+let rec validate (s : Pp.std_ppcmds) = match s with
+  | Pp.Ppcmd_empty
+  | Pp.Ppcmd_print_break _
+  | Pp.Ppcmd_force_newline  -> true
+  | Pp.Ppcmd_glue l    -> List.for_all validate l
+  | Pp.Ppcmd_string s  -> Glib.Utf8.validate s
+  | Pp.Ppcmd_box (_,s)
+  | Pp.Ppcmd_tag (_,s) -> validate s
+  | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s
 
 module Doc = Document
 
@@ -418,9 +421,10 @@ object(self)
     | _ -> false
 
   method private enqueue_feedback msg =
+    (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *)
     let id = msg.id in
     if self#is_dummy_id id then () else Queue.add msg feedbacks
-    
+
   method private process_feedback () =
     let rec eat_feedback n =
       if n = 0 then true else
@@ -466,7 +470,7 @@ object(self)
             (Printf.sprintf "%s %s %s" filepath ident ty)
       | Message(Error, loc, msg), Some (id,sentence) ->
           let loc = Option.default Loc.ghost loc in
-          let msg = Richpp.raw_print msg         in
+          let msg = Pp.string_of_ppcmds msg      in
           log "ErrorMsg" id;
           remove_flag sentence `PROCESSING;
           add_flag sentence (`ERROR (loc, msg));
@@ -476,14 +480,15 @@ object(self)
             self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
       | Message(Warning, loc, msg), Some (id,sentence) ->
           let loc = Option.default Loc.ghost loc in
-          let rmsg = Richpp.raw_print msg         in
-          log "WarningMsg" id;
+          let rmsg = Pp.string_of_ppcmds msg      in
+          log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id;
           add_flag sentence (`WARNING (loc, rmsg));
           self#attach_tooltip sentence loc rmsg;
           self#position_warning_tag_at_sentence sentence loc;
           messages#push Warning msg
       | Message(lvl, loc, msg), Some (id,sentence) ->
-        messages#push lvl msg
+          log ("Msg: " ^ Pp.string_of_ppcmds msg) id;
+          messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
           else to_process <- to_process + n
@@ -629,10 +634,9 @@ object(self)
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] ->
-
-            logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
+            logger Feedback.Error (Pp.str "You must close the proof with Qed or Admitted");
             self#discard_command_queue queue;
-            conclude [] 
+            conclude []
         | `Skip(start,stop), (_,s) :: topstack ->
             assert(start#equal (buffer#get_iter_at_mark s.start));
             assert(stop#equal (buffer#get_iter_at_mark s.stop));
@@ -646,7 +650,7 @@ object(self)
             let handle_answer = function
               | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
                   Doc.assign_tip_id document id;
-                  logger Feedback.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Pp.str msg);
                   self#commit_queue_transaction sentence;
                   loop id []
               | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -654,7 +658,7 @@ object(self)
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
                   self#cleanup (Doc.cut_at document tip);
-                  logger Feedback.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Pp.str msg);
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
                   else loop tip (List.rev topstack)
@@ -673,7 +677,7 @@ object(self)
    let next = function
      | Good _ ->
          messages#clear;
-         messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
+         messages#push Feedback.Info (Pp.str "All proof terms checked by the kernel");
          Coq.return ()
      | Fail x -> self#handle_failure x in
    Coq.bind (Coq.status true) next
@@ -860,7 +864,7 @@ object(self)
       let next = function
       | Fail (_, l, str) -> (* FIXME: check *)
         display_error (l, str);
-        messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase));
+        messages#add (Pp.str ("Unsuccessfully tried: "^phrase));
         more
       | Good msg ->
         messages#add_string msg;
@@ -906,7 +910,7 @@ object(self)
     let get_initial_state =
       let next = function
       | Fail (_, _, message) ->
-        let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in
+        let message = "Couldn't initialize coqtop\n\n" ^ (Pp.string_of_ppcmds message) in
         let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in
         ignore (popup#run ()); exit 1
       | Good id -> initial_state <- id; Coq.return () in