src/Pure/PIDE/xml.scala
changeset 46839 f7232c078fa5
parent 45673 cd41e3903fbf
child 49416 1053a564dd25
     1.1 --- a/src/Pure/PIDE/xml.scala	Thu Mar 08 21:35:54 2012 +0100
     1.2 +++ b/src/Pure/PIDE/xml.scala	Thu Mar 08 21:36:36 2012 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4      private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
     1.5  
     1.6      private def vector(xs: List[String]): XML.Attributes =
     1.7 -      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
     1.8 +      xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) })
     1.9  
    1.10      private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
    1.11        XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
    1.12 @@ -293,15 +293,8 @@
    1.13        }
    1.14  
    1.15      private def vector(atts: XML.Attributes): List[String] =
    1.16 -    {
    1.17 -      val xs = new mutable.ListBuffer[String]
    1.18 -      var i = 0
    1.19 -      for ((a, x) <- atts) {
    1.20 -        if (int_atom(a) == i) { xs += x; i = i + 1 }
    1.21 -        else throw new XML_Atom(a)
    1.22 -      }
    1.23 -      xs.toList
    1.24 -    }
    1.25 +      atts.iterator.zipWithIndex.map(
    1.26 +        { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList
    1.27  
    1.28      private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
    1.29        t match {