src/Pure/PIDE/xml.ML
changeset 46839 f7232c078fa5
parent 46837 5bdd68f380b3
child 46840 42e32c777581
equal deleted inserted replaced
46838:c54b81bb9588 46839:f7232c078fa5
   358 
   358 
   359 fun node (Elem ((":", []), ts)) = ts
   359 fun node (Elem ((":", []), ts)) = ts
   360   | node t = raise XML_BODY [t];
   360   | node t = raise XML_BODY [t];
   361 
   361 
   362 fun vector atts =
   362 fun vector atts =
   363   #1 (fold_map (fn (a, x) =>
   363   map_index (fn (i, (a, x)) => if int_atom a = i then x else raise XML_ATOM a) atts;
   364         fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
       
   365 
   364 
   366 fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   365 fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   367   | tagged t = raise XML_BODY [t];
   366   | tagged t = raise XML_BODY [t];
   368 
   367 
   369 
   368