# HG changeset patch
# User wenzelm
# Date 1310492860 -7200
# Node ID d43e5f79bdc21600fd9b9f9805486d10a65ac96a
# Parent  2cb2310d68b6086574b74bea2cfb05ce3ddaaebc
retain some terminology of "XML attributes";

diff -r 2cb2310d68b6 -r d43e5f79bdc2 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Tue Jul 12 19:36:46 2011 +0200
+++ b/src/Pure/General/xml.ML	Tue Jul 12 19:47:40 2011 +0200
@@ -307,7 +307,7 @@
 val vector =
   fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a);
 
-fun tagged (Elem ((name, props), ts)) = (int_atom name, (#1 (vector props 0), ts))
+fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts))
   | tagged t = raise XML_BODY [t];
 
 
diff -r 2cb2310d68b6 -r d43e5f79bdc2 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Tue Jul 12 19:36:46 2011 +0200
+++ b/src/Pure/General/xml.scala	Tue Jul 12 19:47:40 2011 +0200
@@ -232,7 +232,7 @@
 
     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
 
-    private def vector(xs: List[String]): Properties.T =
+    private def vector(xs: List[String]): XML.Attributes =
       xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
 
     private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
@@ -310,11 +310,11 @@
         case _ => throw new XML_Body(List(t))
       }
 
-    private def vector(props: Properties.T): List[String] =
+    private def vector(atts: XML.Attributes): List[String] =
     {
       val xs = new mutable.ListBuffer[String]
       var i = 0
-      for ((a, x) <- props) {
+      for ((a, x) <- atts) {
         if (int_atom(a) == i) { xs += x; i = i + 1 }
         else throw new XML_Atom(a)
       }
@@ -323,7 +323,7 @@
 
     private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
       t match {
-        case XML.Elem(Markup(name, props), ts) => (int_atom(name), (vector(props), ts))
+        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
         case _ => throw new XML_Body(List(t))
       }