equal
deleted
inserted
replaced
31 (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml); |
31 (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml); |
32 |
32 |
33 val _ = Document.cancel state; |
33 val _ = Document.cancel state; |
34 val (updates, state') = Document.edit old_id new_id edits state; |
34 val (updates, state') = Document.edit old_id new_id edits state; |
35 val _ = |
35 val _ = |
36 implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates) |
36 Output.status (Markup.markup (Markup.assign new_id) |
37 |> Markup.markup (Markup.assign new_id) |
37 (implode (map (Markup.markup_only o Markup.edit) updates))); |
38 |> Output.status; |
|
39 val state'' = Document.execute new_id state'; |
38 val state'' = Document.execute new_id state'; |
40 in state'' end)); |
39 in state'' end)); |
41 |
40 |
42 end; |
41 end; |
43 |
42 |