src/Pure/PIDE/xml.scala
changeset 46839 f7232c078fa5
parent 45673 cd41e3903fbf
child 49416 1053a564dd25
equal deleted inserted replaced
46838:c54b81bb9588 46839:f7232c078fa5
   213     /* structural nodes */
   213     /* structural nodes */
   214 
   214 
   215     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
   215     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
   216 
   216 
   217     private def vector(xs: List[String]): XML.Attributes =
   217     private def vector(xs: List[String]): XML.Attributes =
   218       xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
   218       xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) })
   219 
   219 
   220     private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
   220     private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
   221       XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
   221       XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
   222 
   222 
   223 
   223 
   291         case XML.Elem(Markup(":", Nil), ts) => ts
   291         case XML.Elem(Markup(":", Nil), ts) => ts
   292         case _ => throw new XML_Body(List(t))
   292         case _ => throw new XML_Body(List(t))
   293       }
   293       }
   294 
   294 
   295     private def vector(atts: XML.Attributes): List[String] =
   295     private def vector(atts: XML.Attributes): List[String] =
   296     {
   296       atts.iterator.zipWithIndex.map(
   297       val xs = new mutable.ListBuffer[String]
   297         { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList
   298       var i = 0
       
   299       for ((a, x) <- atts) {
       
   300         if (int_atom(a) == i) { xs += x; i = i + 1 }
       
   301         else throw new XML_Atom(a)
       
   302       }
       
   303       xs.toList
       
   304     }
       
   305 
   298 
   306     private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
   299     private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
   307       t match {
   300       t match {
   308         case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
   301         case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
   309         case _ => throw new XML_Body(List(t))
   302         case _ => throw new XML_Body(List(t))