equal
deleted
inserted
replaced
47 fn (a, []) => Document.Perspective (map int_atom a)])) |
47 fn (a, []) => Document.Perspective (map int_atom a)])) |
48 end; |
48 end; |
49 |
49 |
50 val (removed, assign_update, state') = Document.update old_id new_id edits state; |
50 val (removed, assign_update, state') = Document.update old_id new_id edits state; |
51 val _ = List.app Execution.terminate removed; |
51 val _ = List.app Execution.terminate removed; |
|
52 val _ = Goal.purge_futures removed; |
52 val _ = List.app Isabelle_Process.reset_tracing removed; |
53 val _ = List.app Isabelle_Process.reset_tracing removed; |
53 |
54 |
54 val _ = |
55 val _ = |
55 Output.protocol_message Markup.assign_update |
56 Output.protocol_message Markup.assign_update |
56 ((new_id, assign_update) |> |
57 ((new_id, assign_update) |> |