equal
deleted
inserted
replaced
115 pri = Task_Queue.urgent_pri + 2, interrupts = false} |
115 pri = Task_Queue.urgent_pri + 2, interrupts = false} |
116 (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); |
116 (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); |
117 |
117 |
118 val _ = |
118 val _ = |
119 Output.protocol_message Markup.assign_update |
119 Output.protocol_message Markup.assign_update |
120 [(new_id, assign_update) |> |
120 ((new_id, assign_update) |> |
121 let open XML.Encode |
121 let open XML.Encode |
122 in pair int (list (pair int (list int))) end |
122 in pair int (list (pair int (list int))) end |
123 |> YXML.string_of_body]; |
123 |> YXML.chunks_of_body); |
124 in Document.start_execution state' end))); |
124 in Document.start_execution state' end))); |
125 |
125 |
126 val _ = |
126 val _ = |
127 Isabelle_Process.protocol_command "Document.remove_versions" |
127 Isabelle_Process.protocol_command "Document.remove_versions" |
128 (fn [versions_yxml] => Document.change_state (fn state => |
128 (fn [versions_yxml] => Document.change_state (fn state => |