[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, 0 insertions, 200 deletions

diff --git a/lib/richpp.ml b/lib/richpp.ml
deleted file mode 100644
index c0128dbc2d..0000000000
--- a/lib/richpp.ml
+++ /dev/null
@@ -1,200 +0,0 @@
-(************************************************************************)
-(*  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 Util
-open Xml_datatype
-
-type 'annotation located = {
-  annotation : 'annotation option;
-  startpos   : int;
-  endpos     : int
-}
-
-type 'a stack =
-| Leaf
-| Node of string * 'a located gxml list * int * 'a stack
-
-type 'a context = {
-  mutable stack : 'a stack;
-  (** Pending opened nodes *)
-  mutable offset : int;
-  (** Quantity of characters printed so far *)
-  mutable annotations : 'a option Int.Map.t;
-  (** Map associating annotations to indexes *)
-  mutable index : int;
-  (** Current index of annotations *)
-}
-
-(** We use Format to introduce tags inside the pretty-printed document.
-    Each inserted tag is a fresh index that we keep in sync with the contents
-    of annotations.
-
-    We build an XML tree on the fly, by plugging ourselves in Format tag
-    marking functions. As those functions are called when actually writing to
-    the device, the resulting tree is correct.
-*)
-let rich_pp annotate ppcmds =
-
-  let context = {
-    stack = Leaf;
-    offset = 0;
-    annotations = Int.Map.empty;
-    index = (-1);
-  } in
-
-  let pp_tag obj =
-    let index = context.index + 1 in
-    let () = context.index <- index in
-    let obj = annotate obj in
-    let () = context.annotations <- Int.Map.add index obj context.annotations in
-    string_of_int index
-  in
-
-  let pp_buffer = Buffer.create 180 in
-
-  let push_pcdata () =
-    (** Push the optional PCData on the above node *)
-    let len = Buffer.length pp_buffer in
-    if len = 0 then ()
-    else match context.stack with
-    | Leaf -> assert false
-    | Node (node, child, pos, ctx) ->
-      let data = Buffer.contents pp_buffer in
-      let () = Buffer.clear pp_buffer in
-      let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in
-      context.offset <- context.offset + len
-  in
-
-  let open_xml_tag tag =
-    let () = push_pcdata () in
-    context.stack <- Node (tag, [], context.offset, context.stack)
-  in
-
-  let close_xml_tag tag =
-    let () = push_pcdata () in
-    match context.stack with
-    | Leaf -> assert false
-    | Node (node, child, pos, ctx) ->
-      let () = assert (String.equal tag node) in
-      let annotation =
-        try Int.Map.find (int_of_string node) context.annotations
-        with _ -> None
-      in
-      let annotation = {
-        annotation = annotation;
-        startpos = pos;
-        endpos = context.offset;
-      } in
-      let xml = Element (node, annotation, List.rev child) in
-      match ctx with
-      | Leaf ->
-        (** Final node: we keep the result in a dummy context *)
-        context.stack <- Node ("", [xml], 0, Leaf)
-      | Node (node, child, pos, ctx) ->
-        context.stack <- Node (node, xml :: child, pos, ctx)
-  in
-
-  let open Format in
-
-  let ft = formatter_of_buffer pp_buffer in
-
-  let tag_functions = {
-    mark_open_tag = (fun tag -> let () = open_xml_tag tag in "");
-    mark_close_tag = (fun tag -> let () = close_xml_tag tag in "");
-    print_open_tag = ignore;
-    print_close_tag = ignore;
-  } in
-
-  pp_set_formatter_tag_functions ft tag_functions;
-  pp_set_mark_tags ft true;
-
-  (* Set formatter width. This is currently a hack and duplicate code
-     with Pp_control. Hopefully it will be fixed better in Coq 8.7 *)
-  let w = pp_get_margin str_formatter () in
-  let m = max (64 * w / 100) (w-30) in
-  pp_set_margin ft w;
-  pp_set_max_indent ft m;
-
-  (** The whole output must be a valid document. To that
-      end, we nest the document inside <pp> tags. *)
-  pp_open_tag ft "pp";
-  Pp.(pp_with ~pp_tag ft ppcmds);
-  pp_close_tag ft ();
-
-  (** Get the resulting XML tree. *)
-  let () = pp_print_flush ft () in
-  let () = assert (Buffer.length pp_buffer = 0) in
-  match context.stack with
-  | Node ("", [xml], 0, Leaf) -> xml
-  | _ -> assert false
-
-
-let annotations_positions xml =
-  let rec node accu = function
-    | Element (_, { annotation = Some annotation; startpos; endpos }, cs) ->
-      children ((annotation, (startpos, endpos)) :: accu) cs
-    | Element (_, _, cs) ->
-      children accu cs
-    | _ ->
-      accu
-  and children accu cs =
-    List.fold_left node accu cs
-  in
-  node [] xml
-
-let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
-  let rec node = function
-    | Element (index, { annotation; startpos; endpos }, cs) ->
-      let attributes =
-        [ "startpos", string_of_int startpos;
-          "endpos", string_of_int endpos
-        ]
-        @ (match annotation with
-          | None -> []
-          | Some annotation -> attributes_of_annotation annotation
-        )
-      in
-      let tag =
-        match annotation with
-          | None -> index
-          | Some annotation -> tag_of_annotation annotation
-      in
-      Element (tag, attributes, List.map node cs)
-    | PCData s ->
-      PCData s
-  in
-  node xml
-
-type richpp = xml
-
-let repr xml = xml
-let richpp_of_xml xml = xml
-let richpp_of_string s = PCData s
-
-let richpp_of_pp pp =
-  let annotate t = Some (Ppstyle.repr t)    in
-  let rec drop = function
-  | PCData s -> [PCData s]
-  | Element (_, annotation, cs) ->
-    let cs = List.concat (List.map drop cs) in
-    match annotation.annotation with
-    | None -> cs
-    | Some s -> [Element (String.concat "." s, [], cs)]
-  in
-  let xml = rich_pp annotate pp in
-  Element ("_", [], drop xml)
-
-let raw_print xml =
-  let buf = Buffer.create 1024 in
-  let rec print = function
-  | PCData s -> Buffer.add_string buf s
-  | Element (_, _, cs) -> List.iter print cs
-  in
-  let () = print xml in
-  Buffer.contents buf
-