equal
deleted
inserted
replaced
99 |
99 |
100 |
100 |
101 (* parsing *) |
101 (* parsing *) |
102 |
102 |
103 fun parse_attrib s = |
103 fun parse_attrib s = |
104 (case space_explode "=" s of |
104 (case find_substring "=" s of |
105 [] => err_attribute () |
105 NONE => err_attribute () |
106 | "" :: _ => err_attribute () |
106 | SOME 0 => err_attribute () |
107 | a :: xs => (a, space_implode "=" xs)); |
107 | SOME i => (String.substring (s, 0, i), String.extract (s, i + 1, NONE))); |
108 |
108 |
109 fun parse_chunk ["", ""] = pop |
109 fun parse_chunk ["", ""] = pop |
110 | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts) |
110 | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts) |
111 | parse_chunk txts = fold (add o XML.Text) txts; |
111 | parse_chunk txts = fold (add o XML.Text) txts; |
112 |
112 |