# HG changeset patch
# User wenzelm
# Date 1331233017 -3600
# Node ID 5bdd68f380b37b1ba831c856b24c8ea0eb7e10a5
# Parent  58490158cd74df3e6cef544c275d6f1683e84945
clarified XML signature (again) -- coincide with basic Markup without explicit dependency;

diff -r 58490158cd74 -r 5bdd68f380b3 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Thu Mar 08 17:47:51 2012 +0100
+++ b/src/Pure/PIDE/xml.ML	Thu Mar 08 19:56:57 2012 +0100
@@ -28,9 +28,9 @@
 
 signature XML =
 sig
-  type attributes = Properties.T
+  type attributes = (string * string) list
   datatype tree =
-      Elem of Markup.T * tree list
+      Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
   val add_content: tree -> Buffer.T -> Buffer.T
@@ -59,10 +59,10 @@
 
 (** XML trees **)
 
-type attributes = Properties.T;
+type attributes = (string * string) list;
 
 datatype tree =
-    Elem of Markup.T * tree list
+    Elem of (string * attributes) * tree list
   | Text of string;
 
 type body = tree list;