diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 19:17:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 20:05:34 +0200 |
| commit | 98618cfb6b326b70da29348bc5d212e41086f473 (patch) | |
| tree | b47e7955c5c35f1c415c68fd6a2e97b5745fc32a /lib/xml_datatype.mli | |
| parent | 2c1882815e7877bfc574f9f71eff6ce099145df5 (diff) | |
More parametric type for generalized XML.
Diffstat (limited to 'lib/xml_datatype.mli')
| -rw-r--r-- | lib/xml_datatype.mli | 14 |
1 files changed, 6 insertions, 8 deletions
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 |