--- a/src/Pure/General/xml.ML Sat Dec 02 14:59:25 2006 +0100
+++ b/src/Pure/General/xml.ML Sun Dec 03 16:25:33 2006 +0100
@@ -7,14 +7,16 @@
signature XML =
sig
+ type attributes = (string * string) list
+ datatype tree =
+ Elem of string * attributes * tree list
+ | Text of string
+ type element = string * attributes * tree list
val header: string
val text: string -> string
val text_charref: string -> string
val cdata: string -> string
- val element: string -> (string * string) list -> string list -> string
- datatype tree =
- Elem of string * (string * string) list * tree list
- | Text of string
+ val element: string -> attributes -> string list -> string
val string_of_tree: tree -> string
val parse_content: string list -> tree list * string list
val parse_elem: string list -> tree * string list
@@ -71,10 +73,14 @@
(** explicit XML trees **)
+type attributes = (string * string) list
+
datatype tree =
- Elem of string * (string * string) list * tree list
+ Elem of string * attributes * tree list
| Text of string;
+type element = string * attributes * tree list
+
fun string_of_tree tree =
let
fun string_of (Elem (name, atts, ts)) buf =