equal
deleted
inserted
replaced
51 fn (a, []) => Document.Perspective (map int_atom a)])) |
51 fn (a, []) => Document.Perspective (map int_atom a)])) |
52 end; |
52 end; |
53 |
53 |
54 val (assignment, state') = Document.update old_id new_id edits state; |
54 val (assignment, state') = Document.update old_id new_id edits state; |
55 val _ = |
55 val _ = |
56 Output.protocol_message Isabelle_Markup.assign_execs |
56 Output.protocol_message Markup.assign_execs |
57 ((new_id, assignment) |> |
57 ((new_id, assignment) |> |
58 let open XML.Encode |
58 let open XML.Encode |
59 in pair int (list (pair int (option int))) end |
59 in pair int (list (pair int (option int))) end |
60 |> YXML.string_of_body); |
60 |> YXML.string_of_body); |
61 |
61 |
70 let |
70 let |
71 val versions = |
71 val versions = |
72 YXML.parse_body versions_yxml |> |
72 YXML.parse_body versions_yxml |> |
73 let open XML.Decode in list int end; |
73 let open XML.Decode in list int end; |
74 val state1 = Document.remove_versions versions state; |
74 val state1 = Document.remove_versions versions state; |
75 val _ = Output.protocol_message Isabelle_Markup.removed_versions versions_yxml; |
75 val _ = Output.protocol_message Markup.removed_versions versions_yxml; |
76 in state1 end)); |
76 in state1 end)); |
77 |
77 |
78 val _ = |
78 val _ = |
79 Isabelle_Process.protocol_command "Document.invoke_scala" |
79 Isabelle_Process.protocol_command "Document.invoke_scala" |
80 (fn [id, tag, res] => |
80 (fn [id, tag, res] => |