More invariants in Richpp.

We ensure statically by typing that the tags used by the rich printer
are integers. Furthermore, we also expose through typing that tags are
irrelevants in the returned XML.

4 files changed, 13 insertions, 11 deletions

diff --git a/lib/richpp.ml b/lib/richpp.ml
index 087c247299..7f14ca992e 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -17,7 +17,7 @@ type 'annotation located = {
 
 type 'a stack =
 | Leaf
-| Node of string * (string, 'a located) gxml list * int * 'a stack
+| Node of int * (unit, 'a located) gxml list * int * 'a stack
 
 type 'a context = {
   mutable stack : 'a stack;
@@ -72,6 +72,7 @@ let rich_pp annotate ppcmds =
 
   let open_xml_tag tag =
     let () = push_pcdata () in
+    let tag = try int_of_string tag with _ -> assert false in
     context.stack <- Node (tag, [], context.offset, context.stack)
   in
 
@@ -80,10 +81,11 @@ let rich_pp annotate ppcmds =
     match context.stack with
     | Leaf -> assert false
     | Node (node, child, pos, ctx) ->
-      let () = assert (String.equal tag node) in
+      let tag = try int_of_string tag with _ -> assert false in
+      let () = assert (Int.equal tag node) in
       let annotation =
-        try Int.Map.find (int_of_string node) context.annotations
-        with _ -> None
+        try Int.Map.find node context.annotations
+        with _ -> assert false
       in
       let child = List.rev child in
       let xml = match annotation with
@@ -94,12 +96,12 @@ let rich_pp annotate ppcmds =
           startpos = pos;
           endpos = context.offset;
         } in
-        [Element (node, annotation, child)]
+        [Element ((), annotation, child)]
       in
       match ctx with
       | Leaf ->
         (** Final node: we keep the result in a dummy context *)
-        context.stack <- Node ("", List.rev xml, 0, Leaf)
+        context.stack <- Node ((-1), List.rev xml, 0, Leaf)
       | Node (node, child, pos, ctx) ->
         context.stack <- Node (node, List.rev_append xml child, pos, ctx)
   in
@@ -128,7 +130,7 @@ let rich_pp annotate ppcmds =
   let () = pp_print_flush ft () in
   let () = assert (Buffer.length pp_buffer = 0) in
   match context.stack with
-  | Node ("", [xml], 0, Leaf) -> xml
+  | Node ((-1), [xml], 0, Leaf) -> xml
   | _ -> assert false
 
 
diff --git a/lib/richpp.mli b/lib/richpp.mli
index 5eb0e7b3b0..3f6463c88a 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -23,7 +23,7 @@ type 'annotation located = {
     annotation. If this function returns [None], then no annotation is put. *)
 val rich_pp :
   (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds ->
-  (string, 'annotation located) Xml_datatype.gxml
+  (unit, 'annotation located) Xml_datatype.gxml
 
 (** [annotations_positions ssdoc] returns a list associating each
     annotations with its position in the string from which [ssdoc] is
@@ -37,5 +37,5 @@ val annotations_positions :
 val xml_of_rich_pp :
   ('annotation -> string) ->
   ('annotation -> (string * string) list) ->
-  (string, 'annotation located) Xml_datatype.gxml ->
+  ('a, 'annotation located) Xml_datatype.gxml ->
   Xml_datatype.xml
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index a1c3305bb5..10ca118697 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -5,7 +5,7 @@ module RichppVernac = Ppvernac.Richpp
 module RichppTactic = Pptactic.Richpp
 
 type rich_pp =
-    (string, Ppannotation.t Richpp.located) Xml_datatype.gxml
+    (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml
     * Xml_datatype.xml
 
 let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
diff --git a/printing/richprinter.mli b/printing/richprinter.mli
index 3875e17237..0621e606b6 100644
--- a/printing/richprinter.mli
+++ b/printing/richprinter.mli
@@ -23,7 +23,7 @@ type rich_pp =
 
     (** - a generalized semi-structured document whose attributes are
         annotations ; *)
-    (string, Ppannotation.t Richpp.located) Xml_datatype.gxml
+    (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml
 
     (** - an XML document, representing annotations as usual textual
         XML attributes. *)