equal
deleted
inserted
replaced
31 val edits = |
31 val edits = |
32 YXML.parse_body edits_yxml |> |
32 YXML.parse_body edits_yxml |> |
33 let open XML.Decode in |
33 let open XML.Decode in |
34 list (pair string |
34 list (pair string |
35 (variant |
35 (variant |
36 [fn ([], []) => Document.Clear, |
36 [fn ([], []) => Document.Clear, (* FIXME unused !? *) |
37 fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
37 fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
38 fn ([], a) => |
38 fn ([], a) => |
39 let |
39 let |
40 val (master, (name, (imports, (keywords, (uses, errors))))) = |
40 val (master, (name, (imports, (keywords, (uses, errors))))) = |
41 pair string (pair string (pair (list string) |
41 pair string (pair string (pair (list string) |