Plug the dynamic tags in the Richpp mechanism.

14 files changed, 77 insertions, 109 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 99715b9d3c..336a680bd3 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -153,6 +153,7 @@ Tok
 Lexer
 Ppextend
 Pputils
+Ppannotation
 Stdarg
 Constrarg
 Constrexpr_ops
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
-
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index 5f9dcdc99e..954451397f 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -37,3 +37,5 @@ let tag_of_annotation = function
 
 let attributes_of_annotation a =
   []
+
+let tag = Pp.Tag.create "ppannotation"
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index 9e3ab2b0e2..35f50c144b 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -29,3 +29,5 @@ type t =
 val tag_of_annotation : t -> string
 
 val attributes_of_annotation : t -> (string * string) list
+
+val tag : t Pp.Tag.key
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 9ee81b278e..1481ea191e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -812,15 +812,13 @@ include Make (struct
     let tag_constr_expr = do_not_tag
 end)
 
-module Richpp (Indexer : sig
-  val index : Ppannotation.t -> string
-end) = struct
+module Richpp = struct
 
   include Make (struct
     open Ppannotation
-    let tag_keyword       = Pp.tag (Indexer.index AKeyword)
-    let tag_unparsing unp = Pp.tag (Indexer.index (AUnparsing unp))
-    let tag_constr_expr e = Pp.tag (Indexer.index (AConstrExpr e))
+    let tag_keyword       = Pp.tag (Pp.Tag.inj AKeyword tag)
+    let tag_unparsing unp = Pp.tag (Pp.Tag.inj (AUnparsing unp) tag)
+    let tag_constr_expr e = Pp.tag (Pp.Tag.inj (AConstrExpr e) tag)
   end)
 
 end
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 5f8b2f7360..a480e4e893 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -16,10 +16,6 @@ include Ppconstrsig.Pp
 (** The rich pretty-printers produce {!Pp.std_ppcmds} that are
     interpreted as annotated strings. The annotations can be
     retrieved using {!RichPp.rich_pp}. Their definitions are
-    located in {!Ppannotation.t}.
-
-    Please refer to {!RichPp} to know what are the requirements over
-    [Indexer.index] behavior. *)
-module Richpp (Indexer : sig val index : Ppannotation.t -> string end)
-  : Ppconstrsig.Pp
+    located in {!Ppannotation.t}. *)
 
+module Richpp : Ppconstrsig.Pp
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 9c9bba45b7..520905db9b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1337,20 +1337,18 @@ let _ = Hook.set Tactic_debug.match_rule_printer
     pr_match_rule false (pr_glob_tactic (Global.env()))
       (fun (_,p) -> pr_constr_pattern p) rl)
 
-module Richpp (Indexer : sig
-  val index : Ppannotation.t -> string
-end) = struct
+module Richpp = struct
 
-  include Make (Ppconstr.Richpp (Indexer)) (struct
+  include Make (Ppconstr.Richpp) (struct
     open Ppannotation
-    open Indexer
-    let tag_keyword                   = Pp.tag (Indexer.index AKeyword)
-    let tag_glob_tactic_expr        e = Pp.tag (index (AGlobTacticExpr e))
-    let tag_glob_atomic_tactic_expr a = Pp.tag (index (AGlobAtomicTacticExpr a))
-    let tag_raw_tactic_expr         e = Pp.tag (index (ARawTacticExpr e))
-    let tag_raw_atomic_tactic_expr  a = Pp.tag (index (ARawAtomicTacticExpr a))
-    let tag_tactic_expr             e = Pp.tag (index (ATacticExpr e))
-    let tag_atomic_tactic_expr      a = Pp.tag (index (AAtomicTacticExpr a))
+    let tag e s = Pp.tag (Pp.Tag.inj e tag) s
+    let tag_keyword                   = tag AKeyword
+    let tag_glob_tactic_expr        e = tag (AGlobTacticExpr e)
+    let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a)
+    let tag_raw_tactic_expr         e = tag (ARawTacticExpr e)
+    let tag_raw_atomic_tactic_expr  a = tag (ARawAtomicTacticExpr a)
+    let tag_tactic_expr             e = tag (ATacticExpr e)
+    let tag_atomic_tactic_expr      a = tag (AAtomicTacticExpr a)
   end)
 
 end
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 2003cc1e17..a28c50f831 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -60,10 +60,6 @@ include Pptacticsig.Pp
 (** The rich pretty-printers produce {!Pp.std_ppcmds} that are
     interpreted as annotated strings. The annotations can be
     retrieved using {!RichPp.rich_pp}. Their definitions are
-    located in {!Ppannotation.t}.
-
-    Please refer to {!RichPp} to know what are the requirements over
-    [Indexer.index] behavior. *)
-module Richpp (Indexer : sig val index : Ppannotation.t -> string end)
-  : Pptacticsig.Pp
+    located in {!Ppannotation.t}. *)
+module Richpp : Pptacticsig.Pp
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 21fac8a35c..92d94bdc37 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1272,17 +1272,15 @@ include Make (Ppconstr) (Pptactic) (struct
   let tag_vernac  = do_not_tag
 end)
 
-module Richpp (Indexer : sig
-  val index : Ppannotation.t -> string
-end) = struct
+module Richpp = struct
 
   include Make
-    (Ppconstr.Richpp (Indexer))
-    (Pptactic.Richpp (Indexer))
+    (Ppconstr.Richpp)
+    (Pptactic.Richpp)
     (struct
       open Ppannotation
-      let tag_keyword  = Pp.tag (Indexer.index AKeyword)
-      let tag_vernac v = Pp.tag (Indexer.index (AVernac v))
+      let tag_keyword s = Pp.tag (Pp.Tag.inj AKeyword tag) s
+      let tag_vernac v s = Pp.tag (Pp.Tag.inj (AVernac v) tag) s
      end)
 
 end
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 06f51f0607..976a4ef863 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -16,9 +16,5 @@ include Ppvernacsig.Pp
 (** The rich pretty-printers produce {!Pp.std_ppcmds} that are
     interpreted as annotated strings. The annotations can be
     retrieved using {!RichPp.rich_pp}. Their definitions are
-    located in {!Ppannotation.t}.
-
-    Please refer to {!RichPp} to know what are the requirements over
-    [Indexer.index] behavior. *)
-module Richpp (Indexer : sig val index : Ppannotation.t -> string end)
-  : Ppvernacsig.Pp
+    located in {!Ppannotation.t}. *)
+module Richpp : Ppvernacsig.Pp
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index d27b7c3736..d71dc82d50 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -1,19 +1,19 @@
 open Richpp
 
-module Indexer = Indexer (struct type t = Ppannotation.t end)
-
-module RichppConstr = Ppconstr.Richpp (Indexer)
-module RichppVernac = Ppvernac.Richpp (Indexer)
-module RichppTactic = Pptactic.Richpp (Indexer)
+module RichppConstr = Ppconstr.Richpp
+module RichppVernac = Ppvernac.Richpp
+module RichppTactic = Pptactic.Richpp
 
 type rich_pp =
     string
     * Ppannotation.t Richpp.located Xml_datatype.gxml
     * Xml_datatype.xml
 
+let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
+
 let make_richpp pr ast =
   let raw_pp, rich_pp =
-    rich_pp Indexer.get_annotations (fun () -> pr ast)
+    rich_pp get_annotations (pr ast)
   in
   let xml = Ppannotation.(
     xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp