48 in Document.Header res end, |
48 in Document.Header res end, |
49 fn ([a], []) => Document.Header (Exn.Exn (ERROR a)), |
49 fn ([a], []) => Document.Header (Exn.Exn (ERROR a)), |
50 fn (a, []) => Document.Perspective (map int_atom a)])) |
50 fn (a, []) => Document.Perspective (map int_atom a)])) |
51 end; |
51 end; |
52 |
52 |
53 val (assignment, state1) = Document.update old_id new_id edits state; |
53 val (assignment, state') = Document.update old_id new_id edits state; |
54 val _ = |
54 val _ = |
55 Output.protocol_message Isabelle_Markup.assign_execs |
55 Output.protocol_message Isabelle_Markup.assign_execs |
56 ((new_id, assignment) |> |
56 ((new_id, assignment) |> |
57 let open XML.Encode |
57 let open XML.Encode |
58 in pair int (list (pair int (option int))) end |
58 in pair int (list (pair int (option int))) end |
59 |> YXML.string_of_body); |
59 |> YXML.string_of_body); |
60 val state2 = Document.execute new_id state1; |
60 |
61 in state2 end)); |
61 val _ = Document.start_execution state'; |
|
62 in state' end)); |
62 |
63 |
63 val _ = |
64 val _ = |
64 Isabelle_Process.protocol_command "Document.remove_versions" |
65 Isabelle_Process.protocol_command "Document.remove_versions" |
65 (fn [versions_yxml] => Document.change_state (fn state => |
66 (fn [versions_yxml] => Document.change_state (fn state => |
66 let |
67 let |