equal
deleted
inserted
replaced
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 |