retain some terminology of "XML attributes";
authorwenzelm
Tue Jul 12 19:47:40 2011 +0200 (2011-07-12)
changeset 43781d43e5f79bdc2
parent 43780 2cb2310d68b6
child 43782 834de29572d5
retain some terminology of "XML attributes";
src/Pure/General/xml.ML
src/Pure/General/xml.scala
     1.1 --- a/src/Pure/General/xml.ML	Tue Jul 12 19:36:46 2011 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Tue Jul 12 19:47:40 2011 +0200
     1.3 @@ -307,7 +307,7 @@
     1.4  val vector =
     1.5    fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a);
     1.6  
     1.7 -fun tagged (Elem ((name, props), ts)) = (int_atom name, (#1 (vector props 0), ts))
     1.8 +fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts))
     1.9    | tagged t = raise XML_BODY [t];
    1.10  
    1.11  
     2.1 --- a/src/Pure/General/xml.scala	Tue Jul 12 19:36:46 2011 +0200
     2.2 +++ b/src/Pure/General/xml.scala	Tue Jul 12 19:47:40 2011 +0200
     2.3 @@ -232,7 +232,7 @@
     2.4  
     2.5      private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
     2.6  
     2.7 -    private def vector(xs: List[String]): Properties.T =
     2.8 +    private def vector(xs: List[String]): XML.Attributes =
     2.9        xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
    2.10  
    2.11      private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
    2.12 @@ -310,11 +310,11 @@
    2.13          case _ => throw new XML_Body(List(t))
    2.14        }
    2.15  
    2.16 -    private def vector(props: Properties.T): List[String] =
    2.17 +    private def vector(atts: XML.Attributes): List[String] =
    2.18      {
    2.19        val xs = new mutable.ListBuffer[String]
    2.20        var i = 0
    2.21 -      for ((a, x) <- props) {
    2.22 +      for ((a, x) <- atts) {
    2.23          if (int_atom(a) == i) { xs += x; i = i + 1 }
    2.24          else throw new XML_Atom(a)
    2.25        }
    2.26 @@ -323,7 +323,7 @@
    2.27  
    2.28      private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
    2.29        t match {
    2.30 -        case XML.Elem(Markup(name, props), ts) => (int_atom(name), (vector(props), ts))
    2.31 +        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
    2.32          case _ => throw new XML_Body(List(t))
    2.33        }
    2.34