# HG changeset patch
# User aspinall
# Date 1165159533 -3600
# Node ID 7ab9ad8d67576cc7e9cda7c5277f15b524517460
# Parent  b822c7e61701346485a63901015b905db6303792
Type abbreviations for element args and attributes

diff -r b822c7e61701 -r 7ab9ad8d6757 src/Pure/General/xml.ML
--- 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 =