Revert the four previous commits and update the description of Richpp.

Correcting the code w.r.t. to the API was not the right solution. Instead,
the API comment had to be corrected.

5 files changed, 41 insertions, 37 deletions

diff --git a/lib/richpp.ml b/lib/richpp.ml
index 7f14ca992e..c4a9c39d5a 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -10,14 +10,14 @@ open Util
 open Xml_datatype
 
 type 'annotation located = {
-  annotation : 'annotation;
+  annotation : 'annotation option;
   startpos   : int;
   endpos     : int
 }
 
 type 'a stack =
 | Leaf
-| Node of int * (unit, 'a located) gxml list * int * 'a stack
+| Node of string * 'a located gxml list * int * 'a stack
 
 type 'a context = {
   mutable stack : 'a stack;
@@ -72,7 +72,6 @@ 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
 
@@ -81,29 +80,23 @@ let rich_pp annotate ppcmds =
     match context.stack with
     | Leaf -> assert false
     | Node (node, child, pos, ctx) ->
-      let tag = try int_of_string tag with _ -> assert false in
-      let () = assert (Int.equal tag node) in
+      let () = assert (String.equal tag node) in
       let annotation =
-        try Int.Map.find node context.annotations
-        with _ -> assert false
-      in
-      let child = List.rev child in
-      let xml = match annotation with
-      | None -> child (** Ignore the node *)
-      | Some annotation ->
-        let annotation = {
-          annotation = annotation;
-          startpos = pos;
-          endpos = context.offset;
-        } in
-        [Element ((), annotation, child)]
+        try Int.Map.find (int_of_string node) context.annotations
+        with _ -> None
       in
+      let annotation = {
+        annotation = annotation;
+        startpos = pos;
+        endpos = context.offset;
+      } in
+      let xml = Element (node, annotation, List.rev child) in
       match ctx with
       | Leaf ->
         (** Final node: we keep the result in a dummy context *)
-        context.stack <- Node ((-1), List.rev xml, 0, Leaf)
+        context.stack <- Node ("", [xml], 0, Leaf)
       | Node (node, child, pos, ctx) ->
-        context.stack <- Node (node, List.rev_append xml child, pos, ctx)
+        context.stack <- Node (node, xml :: child, pos, ctx)
   in
 
   let open Format in
@@ -130,14 +123,16 @@ let rich_pp annotate ppcmds =
   let () = pp_print_flush ft () in
   let () = assert (Buffer.length pp_buffer = 0) in
   match context.stack with
-  | Node ((-1), [xml], 0, Leaf) -> xml
+  | Node ("", [xml], 0, Leaf) -> xml
   | _ -> assert false
 
 
 let annotations_positions xml =
   let rec node accu = function
-    | Element (_, { annotation = annotation; startpos; endpos }, cs) ->
+    | Element (_, { annotation = Some annotation; startpos; endpos }, cs) ->
       children ((annotation, (startpos, endpos)) :: accu) cs
+    | Element (_, _, cs) ->
+      children accu cs
     | _ ->
       accu
   and children accu cs =
@@ -152,9 +147,16 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
         [ "startpos", string_of_int startpos;
           "endpos", string_of_int endpos
         ]
-        @ (attributes_of_annotation annotation)
+        @ (match annotation with
+          | None -> []
+          | Some annotation -> attributes_of_annotation annotation
+        )
+      in
+      let tag =
+        match annotation with
+          | None -> index
+          | Some annotation -> tag_of_annotation annotation
       in
-      let tag = tag_of_annotation annotation in
       Element (tag, attributes, List.map node cs)
     | PCData s ->
       PCData s
diff --git a/lib/richpp.mli b/lib/richpp.mli
index 3f6463c88a..a0d3c374b2 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -11,7 +11,7 @@
 (** Each annotation of the semi-structured document refers to the
     substring it annotates. *)
 type 'annotation located = {
-  annotation : 'annotation;
+  annotation : 'annotation option;
   startpos   : int;
   endpos     : int
 }
@@ -20,16 +20,16 @@ type 'annotation located = {
     of [ppcmds] as a semi-structured document
     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. *)
+    annotation. *)
 val rich_pp :
   (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds ->
-  (unit, 'annotation located) Xml_datatype.gxml
+  '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 :
-  ('a, 'annotation located) Xml_datatype.gxml ->
+  'annotation located Xml_datatype.gxml ->
   ('annotation * (int * int)) list
 
 (** [xml_of_rich_pp ssdoc] returns an XML representation of the
@@ -37,5 +37,5 @@ val annotations_positions :
 val xml_of_rich_pp :
   ('annotation -> string) ->
   ('annotation -> (string * string) list) ->
-  ('a, 'annotation located) Xml_datatype.gxml ->
+  'annotation located Xml_datatype.gxml ->
   Xml_datatype.xml
diff --git a/lib/xml_datatype.mli b/lib/xml_datatype.mli
index f822080a6d..f61ba032a2 100644
--- a/lib/xml_datatype.mli
+++ b/lib/xml_datatype.mli
@@ -7,11 +7,13 @@
 (************************************************************************)
 
 (** ['a gxml] is the type for semi-structured documents. They generalize
-    XML by allowing any kind of tags and attributes. *)
-type ('a, 'b) gxml =
-  | Element of ('a * 'b * ('a, 'b) gxml list)
+    XML by allowing any kind of attributes. *)
+type 'a gxml =
+  | Element of (string * 'a * 'a gxml list)
   | PCData of string
 
-(** [xml] is a semi-structured documents where tags are strings and attributes
-    are association lists from string to string. *)
-type xml = (string, (string * string) list) gxml
+(** [xml] is a semi-structured documents where attributes are association
+    lists from string to string. *)
+type xml = (string * string) list gxml
+
+
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index 10ca118697..d95e190749 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -5,7 +5,7 @@ module RichppVernac = Ppvernac.Richpp
 module RichppTactic = Pptactic.Richpp
 
 type rich_pp =
-    (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml
+    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 0621e606b6..41c313514b 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 ; *)
-    (unit, Ppannotation.t Richpp.located) Xml_datatype.gxml
+    Ppannotation.t Richpp.located Xml_datatype.gxml
 
     (** - an XML document, representing annotations as usual textual
         XML attributes. *)