equal
deleted
inserted
replaced
80 Document.Perspective (bool_atom a, map int_atom b, |
80 Document.Perspective (bool_atom a, map int_atom b, |
81 list (pair int (pair string (list string))) c)])) |
81 list (pair int (pair string (list string))) c)])) |
82 end; |
82 end; |
83 |
83 |
84 val (removed, assign_update, state') = Document.update old_id new_id edits state; |
84 val (removed, assign_update, state') = Document.update old_id new_id edits state; |
85 val _ = List.app Execution.terminate removed; |
85 val _ = |
86 val _ = Execution.purge removed; |
86 (singleton o Future.forks) |
87 val _ = List.app Isabelle_Process.reset_tracing removed; |
87 {name = "Document.update/remove", group = NONE, |
|
88 deps = maps Future.group_snapshot (maps Execution.peek removed), |
|
89 pri = 1, interrupts = false} |
|
90 (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); |
88 |
91 |
89 val _ = |
92 val _ = |
90 Output.protocol_message Markup.assign_update |
93 Output.protocol_message Markup.assign_update |
91 [(new_id, assign_update) |> |
94 [(new_id, assign_update) |> |
92 let open XML.Encode |
95 let open XML.Encode |