RichPp: New module.

        It is responsible for turning a tagged pretty-printing into
        a semi-structured document.

clib.mllib: Include RichPp as well as Xml_*.
        The migration of Xml_* from lib to clib is needed by RichPp
        depends on these modules.

4 files changed, 182 insertions, 3 deletions

diff --git a/lib/clib.mllib b/lib/clib.mllib
index 160d49fba..568ffbe0e 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -29,6 +29,10 @@ Util
 Stateid
 Feedback
 Pp
+Xml_lexer
+Xml_parser
+Xml_printer
+RichPp
 CUnix
 Envars
 Aux_file
diff --git a/lib/lib.mllib b/lib/lib.mllib
index b5421a8c8..f3f6ad8fc 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,6 +1,3 @@
-Xml_lexer
-Xml_parser
-Xml_printer
 Errors
 Bigint
 Dyn
diff --git a/lib/richPp.ml b/lib/richPp.ml
new file mode 100644
index 000000000..3f1b17d77
--- /dev/null
+++ b/lib/richPp.ml
@@ -0,0 +1,119 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Xml_datatype
+
+type index = Format.tag
+
+type 'annotation located = {
+  annotation : 'annotation;
+  startpos   : int;
+  endpos     : int
+}
+
+module Indexer (Annotation : sig type t end) = struct
+
+  let annotations : Annotation.t list ref = ref []
+
+  let index =
+    let count = ref (-1) in
+    fun annotation ->
+      incr count;
+      annotations := annotation :: !annotations;
+      string_of_int !count
+
+  let get_annotations () =
+    let annotations = Array.of_list (List.rev !annotations) in
+    fun index -> annotations.(int_of_string index)
+
+end
+
+let rich_pp get_annotations ppcmds =
+  (** First, we use Format to introduce tags inside
+      the pretty-printed document.
+
+      Each inserted tag is an index to an annotation.
+  *)
+  let tagged_pp =
+    let b = Buffer.create 13 in
+    Buffer.add_string b "<pp>";
+    Format.set_tags true;
+    Pp.pp_with (Format.formatter_of_buffer b) ppcmds;
+    Format.set_tags false;
+    Buffer.add_string b "</pp>";
+    Buffer.contents b
+  in
+
+  (** Second, we retrieve the final function that relates
+      each tag to an annotation. *)
+  let get = get_annotations () in
+
+  (** Third, we parse the resulting string. It is a valid XML
+      document (in the sense of Xml_parser). *)
+  let xml_pp = Xml_parser.(parse (make (SString tagged_pp))) in
+
+  (** Fourth, the low-level XML is turned into a high-level
+      semi-structured document that contains a located annotation in
+      every node. During the traversal of the low-level XML document,
+      we build a raw string representation of the pretty-print. *)
+  let rec node buffer = function
+    | Element (index, [], cs) ->
+      let startpos, endpos, cs = children buffer cs in
+      let annotation = get index in
+      (Element (index, { annotation; startpos; endpos }, cs), endpos)
+    | PCData s ->
+      Buffer.add_string buffer s;
+      (PCData s, Buffer.length buffer)
+    | _ ->
+      assert false (* Because of the form of XML produced by Format. *)
+  and children buffer cs =
+    let startpos   = Buffer.length buffer in
+    let cs, endpos =
+      List.fold_left (fun (cs, endpos) c ->
+        let c, endpos = node buffer c in
+        (c :: cs, endpos)
+      ) ([], startpos) cs
+    in
+    (startpos, endpos, List.rev cs)
+  in
+  let pp_buffer = Buffer.create 13 in
+  let xml, _ = node pp_buffer xml_pp in
+
+  (** That's it. We return the raw pretty-printing and its annotations
+      tree. *)
+  (Buffer.contents pp_buffer, xml)
+
+let annotations_positions xml =
+  let rec node accu = function
+    | Element (_, { annotation; startpos; endpos }, cs) ->
+      children ((annotation, (startpos, endpos)) :: 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 (_, { annotation; startpos; endpos }, cs) ->
+      let attributes =
+        [ "startpos", string_of_int startpos;
+          "endpos", string_of_int endpos
+        ]
+        @ attributes_of_annotation annotation
+      in
+      Element (tag_of_annotation annotation,
+               attributes,
+               List.map node cs)
+    | PCData s ->
+      PCData s
+  in
+  node xml
+
+
diff --git a/lib/richPp.mli b/lib/richPp.mli
new file mode 100644
index 000000000..ca7f7a0ba
--- /dev/null
+++ b/lib/richPp.mli
@@ -0,0 +1,59 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module produces semi-structured pretty-printing. *)
+
+(** A pretty printer module must use an instance of the following
+    functor to index annotations. The index must be used as Format.tag
+    during the pretty-printing. *)
+
+(** The indices are Format.tags. *)
+type index = Format.tag (* = string *)
+
+module Indexer (Annotation : sig type t end) : sig
+
+  (** [index annotation] returns a fresh index for the [annotation]. *)
+  val index : Annotation.t -> index
+
+  (** [get_annotations ()] returns a function to retrieve annotations
+      from indices after pretty-printing. *)
+  val get_annotations : unit -> (index -> Annotation.t)
+
+end
+
+(** Each annotation of the semi-structures document refers to the
+    substring it annotates. *)
+type 'annotation located = {
+  annotation : 'annotation;
+  startpos   : int;
+  endpos     : int
+}
+
+(** [rich_pp get_annotations ppcmds] returns the interpretation
+    of [ppcmds] as a string as well as a semi-structured document
+    that represents (located) annotations of this string. *)
+val rich_pp :
+  (unit -> (index -> 'annotation)) ->
+  Pp.std_ppcmds ->
+  string * ('annotation located) Xml_datatype.gxml
+
+(** [annotations_positions ssdoc] returns a list associating each
+    annotations with its position in the string from which [ssdoc] is
+    built. *)
+val annotations_positions :
+  'annotation located Xml_datatype.gxml ->
+  ('annotation * (int * int)) list
+
+(** [xml_of_rich_pp ssdoc] returns an XML representation of the
+    semi-structured document [ssdoc]. *)
+val xml_of_rich_pp :
+  ('annotation -> string) ->
+  ('annotation -> (string * string) list) ->
+  'annotation located Xml_datatype.gxml ->
+  Xml_datatype.xml
+