Plug the dynamic tags in the Richpp mechanism.

4 files changed, 41 insertions, 60 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index a00e70237c..fb092fb6a8 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -127,7 +127,7 @@ type 'a ppcmd_token =
   | Ppcmd_close_box
   | Ppcmd_close_tbox
   | Ppcmd_comment of int
-  | Ppcmd_open_tag of string
+  | Ppcmd_open_tag of Tag.t
   | Ppcmd_close_tag
 
 type 'a ppdir_token =
@@ -293,8 +293,10 @@ let rec pr_com ft s =
           (Format.pp_force_newline ft (); pr_com ft s2)
     | None -> ()
 
+type tag_handler = Tag.t -> Format.tag
+
 (* pretty printing functions *)
-let pp_dirs ft =
+let pp_dirs ?pp_tag ft =
   let pp_open_box = function
     | Pp_hbox n   -> Format.pp_open_hbox ft ()
     | Pp_vbox n   -> Format.pp_open_vbox ft n
@@ -335,10 +337,16 @@ let pp_dirs ft =
 (*        Format.pp_open_hvbox ft 0;*)
         List.iter (pr_com ft) coms(*;
         Format.pp_close_box ft ()*)
-    | Ppcmd_open_tag name ->
-      Format.pp_open_tag ft name
+    | Ppcmd_open_tag tag ->
+      begin match pp_tag with
+      | None -> ()
+      | Some f -> Format.pp_open_tag ft (f tag)
+      end
     | Ppcmd_close_tag ->
-      Format.pp_close_tag ft ()
+      begin match pp_tag with
+      | None -> ()
+      | Some _ -> Format.pp_close_tag ft ()
+      end
   in
   let pp_dir = function
     | Ppdir_ppcmds cmdstream -> Glue.iter pp_cmd cmdstream
@@ -368,8 +376,8 @@ let emacs_quote g =
 
 
 (* pretty printing functions WITHOUT FLUSH *)
-let pp_with ft strm =
-  pp_dirs ft (Glue.atom (Ppdir_ppcmds strm))
+let pp_with ?pp_tag ft strm =
+  pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm))
 
 let ppnl_with ft strm =
   pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ())))
diff --git a/lib/pp.mli b/lib/pp.mli
index d5983c4a21..0293822da4 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -101,8 +101,10 @@ sig
   (** Project an object from a tag. *)
 end
 
-val tag : string -> std_ppcmds -> std_ppcmds
-val open_tag : string -> std_ppcmds
+type tag_handler = Tag.t -> Format.tag
+
+val tag : Tag.t -> std_ppcmds -> std_ppcmds
+val open_tag : Tag.t -> std_ppcmds
 val close_tag : unit -> std_ppcmds
 
 (** {6 Sending messages to the user} *)
@@ -238,9 +240,7 @@ val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 
 (** {6 Low-level pretty-printing functions {% \emph{%}without flush{% }%}. } *)
 
-val pp_with : Format.formatter -> std_ppcmds -> unit
-val ppnl_with : Format.formatter -> std_ppcmds -> unit
-val pp_flush_with : Format.formatter -> unit -> unit
+val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
 
 (** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
 
diff --git a/lib/richpp.ml b/lib/richpp.ml
index f9a7e83a8e..75721df837 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -8,37 +8,27 @@
 
 open Xml_datatype
 
-type index = Format.tag
-
 type 'annotation located = {
   annotation : 'annotation option;
   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 =
+let rich_pp annotate ppcmds =
   (** First, we use Format to introduce tags inside
       the pretty-printed document.
 
-      Each inserted tag is an index to an annotation.
+      Each inserted tag is a fresh index that we keep in sync with the contents
+      of annotations.
   *)
+  let annotations = ref [] in
+  let index = ref (-1) in
+  let pp_tag obj =
+    let () = incr index in
+    let () = annotations := obj :: !annotations in
+    string_of_int !index
+  in
+
   let tagged_pp = Format.(
 
     (** Warning: The following instructions are valid only if
@@ -75,9 +65,9 @@ let rich_pp get_annotations ppcmds =
     (** Some characters must be escaped in XML. This is done by the
         following rewriting of the strings held by pretty-printing
         commands. *)
-    Pp.(pp_with ft (rewrite Xml_printer.pcdata_to_string (ppcmds ())));
+    Pp.(pp_with ~pp_tag ft (rewrite Xml_printer.pcdata_to_string ppcmds));
 
-    (** Insert </p>. *)
+    (** Insert </pp>. *)
     pp_close_tag ft ();
 
     (** Get the final string. *)
@@ -95,7 +85,8 @@ let rich_pp get_annotations ppcmds =
   in
   (** Second, we retrieve the final function that relates
       each tag to an annotation. *)
-  let get = get_annotations () in
+  let objs = CArray.rev_of_list !annotations in
+  let get index = annotate objs.(index) in
 
   (** Third, we parse the resulting string. It is a valid XML
       document (in the sense of Xml_parser). As blanks are
@@ -121,7 +112,7 @@ let rich_pp get_annotations ppcmds =
   let rec node buffer = function
     | Element (index, [], cs) ->
       let startpos, endpos, cs = children buffer cs in
-      let annotation = try Some (get index) with _ -> None in
+      let annotation = try get (int_of_string index) with _ -> None in
       (Element (index, { annotation; startpos; endpos }, cs), endpos)
 
     | PCData s ->
diff --git a/lib/richpp.mli b/lib/richpp.mli
index 834115d40b..cc1cd63213 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -8,24 +8,6 @@
 
 (** This module offers semi-structured pretty-printing. *)
 
-(** A pretty printer module must use an instance of the following
-    functor to index annotations. The index is to be used as a
-    [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-structured document refers to the
     substring it annotates. *)
 type 'annotation located = {
@@ -36,11 +18,12 @@ type 'annotation located = {
 
 (** [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. *)
+    that represents (located) annotations of this string.
+    The [get_annotations] function is used to convert tags into the desired
+    annotation. If this function returns [None], then no annotation is put. *)
 val rich_pp :
-  (unit -> (index -> 'annotation)) ->
-  (unit -> Pp.std_ppcmds) ->
-  string * ('annotation located) Xml_datatype.gxml
+  (Pp.Tag.t -> 'annotation option) -> 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
@@ -56,4 +39,3 @@ val xml_of_rich_pp :
   ('annotation -> (string * string) list) ->
   'annotation located Xml_datatype.gxml ->
   Xml_datatype.xml
-