aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-08-15 19:17:26 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-08-15 20:05:34 +0200
commit98618cfb6b326b70da29348bc5d212e41086f473 (patch)
treeb47e7955c5c35f1c415c68fd6a2e97b5745fc32a /lib
parent2c1882815e7877bfc574f9f71eff6ce099145df5 (diff)
More parametric type for generalized XML.
Diffstat (limited to 'lib')
-rw-r--r--lib/richpp.ml2
-rw-r--r--lib/richpp.mli6
-rw-r--r--lib/xml_datatype.mli14
3 files changed, 10 insertions, 12 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