[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, 57 insertions, 14 deletions

diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 65f44fdd38..08f23d3d4e 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -97,6 +97,49 @@ let to_richpp xml = match xml with
   | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x
   | x -> raise Serialize.(Marshal_error("richpp",x))
 
+let of_box (ppb : Pp.block_type) = let open Pp in match ppb with
+  | Pp_hbox   i -> constructor "ppbox" "hbox"   [of_int i]
+  | Pp_vbox   i -> constructor "ppbox" "vbox"   [of_int i]
+  | Pp_hvbox  i -> constructor "ppbox" "hvbox"  [of_int i]
+  | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i]
+
+let to_box = let open Pp in
+  do_match "ppbox" (fun s args -> match s with
+      | "hbox"   -> Pp_hbox   (to_int (singleton args))
+      | "vbox"   -> Pp_vbox   (to_int (singleton args))
+      | "hvbox"  -> Pp_hvbox  (to_int (singleton args))
+      | "hovbox" -> Pp_hovbox (to_int (singleton args))
+      | x        -> raise (Marshal_error("*ppbox",PCData x))
+    )
+
+let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with
+    | Ppcmd_empty         -> constructor "ppdoc" "emtpy"  []
+    | Ppcmd_string s      -> constructor "ppdoc" "string" [of_string s]
+    | Ppcmd_glue sl       -> constructor "ppdoc" "glue"   [of_list of_pp sl]
+    | Ppcmd_box (bt,s)    -> constructor "ppdoc" "box"    [of_pair of_box of_pp (bt,s)]
+    | Ppcmd_tag (t,s)     -> constructor "ppdoc" "tag"    [of_pair (of_list of_string) of_pp (t,s)]
+    | Ppcmd_print_break (i,j)
+                          -> constructor "ppdoc" "break"     [of_pair of_int of_int (i,j)]
+    | Ppcmd_force_newline -> constructor "ppdoc" "newline"   []
+    | Ppcmd_comment cmd   -> constructor "ppdoc" "comment" [of_list of_string cmd]
+
+
+let rec to_pp xpp = let open Pp in
+  do_match "ppdoc" (fun s args -> match s with
+    | "empty"     -> Ppcmd_empty
+    | "string"    -> Ppcmd_string (to_string (singleton args))
+    | "glue"      -> Ppcmd_glue (to_list to_pp (singleton args))
+    | "box"       -> let (bt,s) = to_pair to_box to_pp (singleton args) in
+                     Ppcmd_box(bt,s)
+    | "tag"       -> let (tg,s) = to_pair (to_list to_string) to_pp (singleton args) in
+                     Ppcmd_tag(tg,s)
+    | "break"     -> let (i,j)   = to_pair to_int to_int (singleton args) in
+                     Ppcmd_print_break(i, j)
+    | "newline"   -> Ppcmd_force_newline
+    | "comment"   -> Ppcmd_comment (to_list to_string (singleton args))
+    | x           -> raise (Marshal_error("*ppdoc",PCData x))
+  ) xpp
+
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
 | Fail (id,loc, msg) ->
@@ -104,7 +147,7 @@ let of_value f = function
   | None -> []
   | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
   let id = of_stateid id in
-  Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg])
+  Element ("value", ["val", "fail"] @ loc, [id; of_pp msg])
 
 let to_value f = function
 | Element ("value", attrs, l) ->
@@ -120,7 +163,7 @@ let to_value f = function
     in
     let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in
     let id = to_stateid id in
-    let msg = to_richpp msg in
+    let msg = to_pp msg    in
     Fail (id, loc, msg)
   else raise (Marshal_error("good or fail",PCData ans))
 | x -> raise (Marshal_error("value",x))
@@ -147,15 +190,15 @@ let to_evar = function
   | x -> raise (Marshal_error("evar",x))
 
 let of_goal g =
-  let hyp = of_list of_richpp g.goal_hyp in
-  let ccl = of_richpp g.goal_ccl in
+  let hyp = of_list of_pp g.goal_hyp in
+  let ccl = of_pp g.goal_ccl in
   let id = of_string g.goal_id in
   Element ("goal", [], [id; hyp; ccl])
 let to_goal = function
   | Element ("goal", [], [id; hyp; ccl]) ->
-    let hyp = to_list to_richpp hyp in
-    let ccl = to_richpp ccl in
-    let id = to_string id in
+    let hyp = to_list to_pp hyp in
+    let ccl = to_pp ccl         in
+    let id  = to_string id      in
     { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
   | x -> raise (Marshal_error("goal",x))
 
@@ -344,8 +387,8 @@ end = struct
         Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
     else
       let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
-        "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^
-            Richpp.raw_print goal ^ "]" in
+        "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^
+            Pp.string_of_ppcmds goal ^ "]" in
       String.concat " " (List.map pr_goal g.fg_goals)
   let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
   let pr_status (s : status) =
@@ -701,10 +744,10 @@ let to_call : xml -> unknown_call =
 
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
-  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]"
+  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]"
   | Fail (id,Some(i,j),str) ->
       "FAIL "^Stateid.to_string id^
-        " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]"
+        " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]"
 let pr_value v = pr_value_gen (fun _ -> "FIXME") v
 let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with
   | Add _        -> pr_value_gen (print add_rty_t        ) value
@@ -760,7 +803,7 @@ let document to_string_fmt =
     (to_string_fmt (of_value (fun _ -> PCData "b") (Good ())));
   Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n"
     (to_string_fmt (of_value (fun _ -> PCData "b")
-      (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message"))));
+      (Fail (Stateid.initial,Some (15,34), Pp.str "error message"))));
   document_type_encoding to_string_fmt
 
 (* Moved from feedback.mli : This is IDE specific and we don't want to
@@ -787,12 +830,12 @@ let to_message_level =
 let of_message lvl loc msg =
   let lvl     = of_message_level lvl in
   let xloc    = of_option of_loc loc in
-  let content = of_richpp msg        in
+  let content = of_pp msg            in
   Xml_datatype.Element ("message", [], [lvl; xloc; content])
 
 let to_message xml = match xml with
   | Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
-      Message(to_message_level lvl, to_option to_loc xloc, to_richpp content)
+      Message(to_message_level lvl, to_option to_loc xloc, to_pp content)
   | x -> raise (Marshal_error("message",x))
 
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with