diff options
| -rw-r--r-- | lib/richpp.ml | 2 | ||||
| -rw-r--r-- | lib/richpp.mli | 6 | ||||
| -rw-r--r-- | lib/xml_datatype.mli | 14 | ||||
| -rw-r--r-- | printing/richprinter.ml | 2 | ||||
| -rw-r--r-- | printing/richprinter.mli | 2 |
5 files changed, 12 insertions, 14 deletions
diff --git a/lib/richpp.ml b/lib/richpp.ml index 45173ff30..087c24729 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -17,7 +17,7 @@ type 'annotation located = { type 'a stack = | Leaf -| Node of string * 'a located gxml list * int * 'a stack +| Node of string * (string, 'a located) gxml list * int * 'a stack type 'a context = { mutable stack : 'a stack; diff --git a/lib/richpp.mli b/lib/richpp.mli index 2c2019789..5eb0e7b3b 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -23,13 +23,13 @@ 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 -> - 'annotation located Xml_datatype.gxml + (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 built. *) val annotations_positions : - 'annotation located Xml_datatype.gxml -> + ('a, '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) -> - 'annotation located Xml_datatype.gxml -> + (string, 'annotation located) Xml_datatype.gxml -> Xml_datatype.xml diff --git a/lib/xml_datatype.mli b/lib/xml_datatype.mli index f61ba032a..f822080a6 100644 --- a/lib/xml_datatype.mli +++ b/lib/xml_datatype.mli @@ -7,13 +7,11 @@ (************************************************************************) (** ['a gxml] is the type for semi-structured documents. They generalize - XML by allowing any kind of attributes. *) -type 'a gxml = - | Element of (string * 'a * 'a gxml list) + XML by allowing any kind of tags and attributes. *) +type ('a, 'b) gxml = + | Element of ('a * 'b * ('a, 'b) gxml list) | PCData of string -(** [xml] is a semi-structured documents where attributes are association - lists from string to string. *) -type xml = (string * string) list gxml - - +(** [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 diff --git a/printing/richprinter.ml b/printing/richprinter.ml index d95e19074..a1c3305bb 100644 --- a/printing/richprinter.ml +++ b/printing/richprinter.ml @@ -5,7 +5,7 @@ module RichppVernac = Ppvernac.Richpp module RichppTactic = Pptactic.Richpp type rich_pp = - Ppannotation.t Richpp.located Xml_datatype.gxml + (string, 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 41c313514..3875e1723 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 ; *) - Ppannotation.t Richpp.located Xml_datatype.gxml + (string, Ppannotation.t Richpp.located) Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) |