diff options
| author | Pierre-Marie Pédrot | 2015-08-15 19:17:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-08-15 20:05:34 +0200 |
| commit | 98618cfb6b326b70da29348bc5d212e41086f473 (patch) | |
| tree | b47e7955c5c35f1c415c68fd6a2e97b5745fc32a /lib/richpp.mli | |
| parent | 2c1882815e7877bfc574f9f71eff6ce099145df5 (diff) | |
More parametric type for generalized XML.
Diffstat (limited to 'lib/richpp.mli')
| -rw-r--r-- | lib/richpp.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/richpp.mli b/lib/richpp.mli index 2c20197893..5eb0e7b3b0 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 |