diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-10-30 22:13:21 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:35 +0100 |
| commit | 812c611bdc8532b7cd25d9368a8356be3eb1d34a (patch) | |
| tree | 14c49e92d23052afcb4a802dd531d2bdf23f2118 /lib/xml_datatype.mli | |
| parent | d21183a81fb73cd20ace5213cfe46c82250db38b (diff) | |
Xml_datatype.gxml: New type for semi-structured documents.
Xml_parser, Xml_printer: Use it.
Diffstat (limited to 'lib/xml_datatype.mli')
| -rw-r--r-- | lib/xml_datatype.mli | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/lib/xml_datatype.mli b/lib/xml_datatype.mli index 7b18c73bf..3d0e897ac 100644 --- a/lib/xml_datatype.mli +++ b/lib/xml_datatype.mli @@ -6,7 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type xml = - | Element of (string * (string * string) list * xml list) - | PCData of string +(** ['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) + | PCData of string + +(** [xml] is a semi-structured documents where attributes are association + lists from string to string. *) +type xml = (string * string) list gxml + |