From 812c611bdc8532b7cd25d9368a8356be3eb1d34a Mon Sep 17 00:00:00 2001 From: Regis-Gianas Date: Thu, 30 Oct 2014 22:13:21 +0100 Subject: Xml_datatype.gxml: New type for semi-structured documents. Xml_parser, Xml_printer: Use it. --- lib/xml_datatype.mli | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'lib/xml_datatype.mli') 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 + -- cgit v1.2.3