Plug the dynamic tags in the Richpp mechanism.

9 files changed, 35 insertions, 49 deletions

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